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

Theorem ptolemy 23463
 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 14238, then using algebraic simplification to show that both sides are equal. This formalization is based on the proof in "Trigonometry" by Gelfand and Saul. This is Metamath 100 proof #95. (Contributed by David A. Wheeler, 31-May-2015.)
Assertion
Ref Expression
ptolemy

Proof of Theorem ptolemy
StepHypRef Expression
1 addcl 9626 . . . . . . . . . . 11
213ad2ant2 1031 . . . . . . . . . 10
32coscld 14197 . . . . . . . . 9
43negnegd 9982 . . . . . . . 8
5 addid2 9821 . . . . . . . . . . . . . . 15
65oveq1d 6310 . . . . . . . . . . . . . 14
72, 6syl 17 . . . . . . . . . . . . 13
8 0cnd 9641 . . . . . . . . . . . . . 14
9 addcl 9626 . . . . . . . . . . . . . . . 16
109adantr 467 . . . . . . . . . . . . . . 15
11103adant3 1029 . . . . . . . . . . . . . 14
128, 11, 2pnpcan2d 10029 . . . . . . . . . . . . 13
13 simp3 1011 . . . . . . . . . . . . . 14
1413oveq2d 6311 . . . . . . . . . . . . 13
157, 12, 143eqtr3rd 2496 . . . . . . . . . . . 12
16 df-neg 9868 . . . . . . . . . . . 12
1715, 16syl6eqr 2505 . . . . . . . . . . 11
1817fveq2d 5874 . . . . . . . . . 10
19 cosmpi 23455 . . . . . . . . . . 11
202, 19syl 17 . . . . . . . . . 10
21 cosneg 14213 . . . . . . . . . . 11
2211, 21syl 17 . . . . . . . . . 10
2318, 20, 223eqtr3d 2495 . . . . . . . . 9
2423negeqd 9874 . . . . . . . 8
254, 24eqtr3d 2489 . . . . . . 7
2625oveq2d 6311 . . . . . 6
27 subcl 9879 . . . . . . . . . 10
2827adantl 468 . . . . . . . . 9
2928coscld 14197 . . . . . . . 8
30293adant3 1029 . . . . . . 7
3111coscld 14197 . . . . . . 7
3230, 31subnegd 9998 . . . . . 6
3326, 32eqtrd 2487 . . . . 5
3433oveq1d 6310 . . . 4
3534oveq2d 6311 . . 3
36 subcl 9879 . . . . . . . 8
37363ad2ant1 1030 . . . . . . 7
3837coscld 14197 . . . . . 6
3938, 31subcld 9991 . . . . 5
4030, 31addcld 9667 . . . . 5
41 2cnne0 10831 . . . . . 6
4241a1i 11 . . . . 5
43 divdir 10300 . . . . 5
4439, 40, 42, 43syl3anc 1269 . . . 4
4538, 31, 30nppcan3d 10018 . . . . 5
4645oveq1d 6310 . . . 4
4744, 46eqtr3d 2489 . . 3
4835, 47eqtrd 2487 . 2
49 sinmul 14238 . . . 4
51 sinmul 14238 . . . 4
5350, 52oveq12d 6313 . 2
54 simplr 763 . . . . . . . . 9
55 simpll 761 . . . . . . . . 9
56 simprl 765 . . . . . . . . 9
5754, 55, 56pnpcan2d 10029 . . . . . . . 8
5857fveq2d 5874 . . . . . . 7
59583adant3 1029 . . . . . 6
601adantl 468 . . . . . . . . . . . . 13
6110, 60, 283jca 1189 . . . . . . . . . . . 12
62613adant3 1029 . . . . . . . . . . 11
63 addass 9631 . . . . . . . . . . 11
6462, 63syl 17 . . . . . . . . . 10
65 oveq1 6302 . . . . . . . . . . 11
66653ad2ant3 1032 . . . . . . . . . 10
67 simpl 459 . . . . . . . . . . . . . 14
68 simpr 463 . . . . . . . . . . . . . 14
6967, 68, 673jca 1189 . . . . . . . . . . . . 13
70693ad2ant2 1031 . . . . . . . . . . . 12
71 ppncan 9921 . . . . . . . . . . . . 13
7271oveq2d 6311 . . . . . . . . . . . 12
7370, 72syl 17 . . . . . . . . . . 11
74 simp1 1009 . . . . . . . . . . . 12
7567, 67jca 535 . . . . . . . . . . . . 13
76753ad2ant2 1031 . . . . . . . . . . . 12
77 add4 9854 . . . . . . . . . . . 12
7874, 76, 77syl2anc 667 . . . . . . . . . . 11
79 addcl 9626 . . . . . . . . . . . . . . 15
8079ad2ant2r 754 . . . . . . . . . . . . . 14
81 addcl 9626 . . . . . . . . . . . . . . 15
8281ad2ant2lr 755 . . . . . . . . . . . . . 14
8380, 82jca 535 . . . . . . . . . . . . 13
84833adant3 1029 . . . . . . . . . . . 12
85 addcom 9824 . . . . . . . . . . . 12
8684, 85syl 17 . . . . . . . . . . 11
8773, 78, 863eqtrd 2491 . . . . . . . . . 10
8864, 66, 873eqtr3rd 2496 . . . . . . . . 9
89 picn 23426 . . . . . . . . . . 11
90 addcom 9824 . . . . . . . . . . 11
9189, 28, 90sylancr 670 . . . . . . . . . 10
92913adant3 1029 . . . . . . . . 9
9388, 92eqtrd 2487 . . . . . . . 8
9493fveq2d 5874 . . . . . . 7
95 cosppi 23457 . . . . . . . . 9
9628, 95syl 17 . . . . . . . 8
97963adant3 1029 . . . . . . 7
9894, 97eqtrd 2487 . . . . . 6
9959, 98oveq12d 6313 . . . . 5
100 subcl 9879 . . . . . . . . . 10
101100ancoms 455 . . . . . . . . 9
102101adantr 467 . . . . . . . 8
103102coscld 14197 . . . . . . 7
104103, 29subnegd 9998 . . . . . 6
1051043adant3 1029 . . . . 5
10699, 105eqtrd 2487 . . . 4
107106oveq1d 6310 . . 3
108 sinmul 14238 . . . . 5
10982, 80, 108syl2anc 667 . . . 4