Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptolemy Unicode version

Theorem ptolemy 19696
 Description: Ptolemy's Theorem. This theorem is named after the Greek astronomer and mathematician Ptolemy (Claudius Ptolemaeus). This particular version is expressed using the sine function. It is proved by expanding all the multiplication of sines to a product of cosines of differences using sinmul 12326, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. (Contributed by David A. Wheeler, 31-May-2015.)
Assertion
Ref Expression
ptolemy

Proof of Theorem ptolemy
StepHypRef Expression
1 addcl 8699 . . . . . . . . . . 11
213ad2ant2 982 . . . . . . . . . 10
32coscld 12285 . . . . . . . . 9
43negnegd 9028 . . . . . . . 8
5 cosmpi 19688 . . . . . . . . . . 11
62, 5syl 17 . . . . . . . . . 10
7 addid2 8875 . . . . . . . . . . . . . . . 16
87oveq1d 5725 . . . . . . . . . . . . . . 15
92, 8syl 17 . . . . . . . . . . . . . 14
10 0cn 8711 . . . . . . . . . . . . . . . 16
1110a1i 12 . . . . . . . . . . . . . . 15
12 addcl 8699 . . . . . . . . . . . . . . . . 17
1312adantr 453 . . . . . . . . . . . . . . . 16
14133adant3 980 . . . . . . . . . . . . . . 15
1511, 14, 2pnpcan2d 9075 . . . . . . . . . . . . . 14
16 simp3 962 . . . . . . . . . . . . . . 15
1716oveq2d 5726 . . . . . . . . . . . . . 14
189, 15, 173eqtr3rd 2294 . . . . . . . . . . . . 13
19 df-neg 8920 . . . . . . . . . . . . 13
2018, 19syl6eqr 2303 . . . . . . . . . . . 12
2120fveq2d 5381 . . . . . . . . . . 11
22 cosneg 12301 . . . . . . . . . . . 12
2314, 22syl 17 . . . . . . . . . . 11
2421, 23eqtrd 2285 . . . . . . . . . 10
256, 24eqtr3d 2287 . . . . . . . . 9
2625negeqd 8926 . . . . . . . 8
274, 26eqtr3d 2287 . . . . . . 7
2827oveq2d 5726 . . . . . 6
29 subcl 8931 . . . . . . . . . 10
3029adantl 454 . . . . . . . . 9
3130coscld 12285 . . . . . . . 8
32313adant3 980 . . . . . . 7
3314coscld 12285 . . . . . . 7
3432, 33subnegd 9044 . . . . . 6
3528, 34eqtrd 2285 . . . . 5
3635oveq1d 5725 . . . 4
3736oveq2d 5726 . . 3
38 subcl 8931 . . . . . . . 8
39383ad2ant1 981 . . . . . . 7
4039coscld 12285 . . . . . 6
4140, 33subcld 9037 . . . . 5
4232, 33addcld 8734 . . . . 5
43 2cn 9696 . . . . . . 7
44 2ne0 9709 . . . . . . 7
4543, 44pm3.2i 443 . . . . . 6
4645a1i 12 . . . . 5
47 divdir 9327 . . . . 5
4841, 42, 46, 47syl3anc 1187 . . . 4
4940, 33, 32nppcan3d 9064 . . . . 5
5049oveq1d 5725 . . . 4
5148, 50eqtr3d 2287 . . 3
5237, 51eqtrd 2285 . 2
53 sinmul 12326 . . . 4
55 sinmul 12326 . . . 4
5754, 56oveq12d 5728 . 2
58 simplr 734 . . . . . . . . 9
59 simpll 733 . . . . . . . . 9
60 simprl 735 . . . . . . . . 9
6158, 59, 60pnpcan2d 9075 . . . . . . . 8
6261fveq2d 5381 . . . . . . 7
63623adant3 980 . . . . . 6
641adantl 454 . . . . . . . . . . . . 13
6513, 64, 303jca 1137 . . . . . . . . . . . 12
66653adant3 980 . . . . . . . . . . 11
67 addass 8704 . . . . . . . . . . 11
6866, 67syl 17 . . . . . . . . . 10
69 oveq1 5717 . . . . . . . . . . 11
70693ad2ant3 983 . . . . . . . . . 10
71 simpl 445 . . . . . . . . . . . . . 14
72 simpr 449 . . . . . . . . . . . . . 14
7371, 72, 713jca 1137 . . . . . . . . . . . . 13
74733ad2ant2 982 . . . . . . . . . . . 12
75 ppncan 8969 . . . . . . . . . . . . 13
7675oveq2d 5726 . . . . . . . . . . . 12
7774, 76syl 17 . . . . . . . . . . 11
78 simp1 960 . . . . . . . . . . . 12
7971, 71jca 520 . . . . . . . . . . . . 13
80793ad2ant2 982 . . . . . . . . . . . 12
81 add4 8907 . . . . . . . . . . . 12
8278, 80, 81syl2anc 645 . . . . . . . . . . 11
83 addcl 8699 . . . . . . . . . . . . . . 15
8483ad2ant2r 730 . . . . . . . . . . . . . 14
85 addcl 8699 . . . . . . . . . . . . . . 15
8685ad2ant2lr 731 . . . . . . . . . . . . . 14
8784, 86jca 520 . . . . . . . . . . . . 13
88873adant3 980 . . . . . . . . . . . 12
89 addcom 8878 . . . . . . . . . . . 12
9088, 89syl 17 . . . . . . . . . . 11
9177, 82, 903eqtrd 2289 . . . . . . . . . 10
9268, 70, 913eqtr3rd 2294 . . . . . . . . 9
93 pire 19664 . . . . . . . . . . . 12
9493recni 8729 . . . . . . . . . . 11
95 addcom 8878 . . . . . . . . . . 11
9694, 30, 95sylancr 647 . . . . . . . . . 10
97963adant3 980 . . . . . . . . 9
9892, 97eqtrd 2285 . . . . . . . 8
9998fveq2d 5381 . . . . . . 7
100 cosppi 19690 . . . . . . . . 9
10130, 100syl 17 . . . . . . . 8
1021013adant3 980 . . . . . . 7
10399, 102eqtrd 2285 . . . . . 6
10463, 103oveq12d 5728 . . . . 5
105 subcl 8931 . . . . . . . . . 10
106105ancoms 441 . . . . . . . . 9
107106adantr 453 . . . . . . . 8
108107coscld 12285 . . . . . . 7
109108, 31subnegd 9044 . . . . . 6
1101093adant3 980 . . . . 5
111104, 110eqtrd 2285 . . . 4
112111oveq1d 5725 . . 3
113 sinmul 12326 . . . . 5
11486, 84, 113syl2anc 645 . . . 4