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

Theorem ptolemy 20409
 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 12778, 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 9077 . . . . . . . . . . 11
213ad2ant2 980 . . . . . . . . . 10
32coscld 12737 . . . . . . . . 9
43negnegd 9407 . . . . . . . 8
5 addid2 9254 . . . . . . . . . . . . . . 15
65oveq1d 6099 . . . . . . . . . . . . . 14
72, 6syl 16 . . . . . . . . . . . . 13
8 0cn 9089 . . . . . . . . . . . . . . 15
98a1i 11 . . . . . . . . . . . . . 14
10 addcl 9077 . . . . . . . . . . . . . . . 16
1110adantr 453 . . . . . . . . . . . . . . 15
12113adant3 978 . . . . . . . . . . . . . 14
139, 12, 2pnpcan2d 9454 . . . . . . . . . . . . 13
14 simp3 960 . . . . . . . . . . . . . 14
1514oveq2d 6100 . . . . . . . . . . . . 13
167, 13, 153eqtr3rd 2479 . . . . . . . . . . . 12
17 df-neg 9299 . . . . . . . . . . . 12
1816, 17syl6eqr 2488 . . . . . . . . . . 11
1918fveq2d 5735 . . . . . . . . . 10
20 cosmpi 20401 . . . . . . . . . . 11
212, 20syl 16 . . . . . . . . . 10
22 cosneg 12753 . . . . . . . . . . 11
2312, 22syl 16 . . . . . . . . . 10
2419, 21, 233eqtr3d 2478 . . . . . . . . 9
2524negeqd 9305 . . . . . . . 8
264, 25eqtr3d 2472 . . . . . . 7
2726oveq2d 6100 . . . . . 6
28 subcl 9310 . . . . . . . . . 10
2928adantl 454 . . . . . . . . 9
3029coscld 12737 . . . . . . . 8
31303adant3 978 . . . . . . 7
3212coscld 12737 . . . . . . 7
3331, 32subnegd 9423 . . . . . 6
3427, 33eqtrd 2470 . . . . 5
3534oveq1d 6099 . . . 4
3635oveq2d 6100 . . 3
37 subcl 9310 . . . . . . . 8
38373ad2ant1 979 . . . . . . 7
3938coscld 12737 . . . . . 6
4039, 32subcld 9416 . . . . 5
4131, 32addcld 9112 . . . . 5
42 2cn 10075 . . . . . . 7
43 2ne0 10088 . . . . . . 7
4442, 43pm3.2i 443 . . . . . 6
4544a1i 11 . . . . 5
46 divdir 9706 . . . . 5
4740, 41, 45, 46syl3anc 1185 . . . 4
4839, 32, 31nppcan3d 9443 . . . . 5
4948oveq1d 6099 . . . 4
5047, 49eqtr3d 2472 . . 3
5136, 50eqtrd 2470 . 2
52 sinmul 12778 . . . 4
54 sinmul 12778 . . . 4
5653, 55oveq12d 6102 . 2
57 simplr 733 . . . . . . . . 9
58 simpll 732 . . . . . . . . 9
59 simprl 734 . . . . . . . . 9
6057, 58, 59pnpcan2d 9454 . . . . . . . 8
6160fveq2d 5735 . . . . . . 7
62613adant3 978 . . . . . 6
631adantl 454 . . . . . . . . . . . . 13
6411, 63, 293jca 1135 . . . . . . . . . . . 12
65643adant3 978 . . . . . . . . . . 11
66 addass 9082 . . . . . . . . . . 11
6765, 66syl 16 . . . . . . . . . 10
68 oveq1 6091 . . . . . . . . . . 11
69683ad2ant3 981 . . . . . . . . . 10
70 simpl 445 . . . . . . . . . . . . . 14
71 simpr 449 . . . . . . . . . . . . . 14
7270, 71, 703jca 1135 . . . . . . . . . . . . 13
73723ad2ant2 980 . . . . . . . . . . . 12
74 ppncan 9348 . . . . . . . . . . . . 13
7574oveq2d 6100 . . . . . . . . . . . 12
7673, 75syl 16 . . . . . . . . . . 11
77 simp1 958 . . . . . . . . . . . 12
7870, 70jca 520 . . . . . . . . . . . . 13
79783ad2ant2 980 . . . . . . . . . . . 12
80 add4 9286 . . . . . . . . . . . 12
8177, 79, 80syl2anc 644 . . . . . . . . . . 11
82 addcl 9077 . . . . . . . . . . . . . . 15
8382ad2ant2r 729 . . . . . . . . . . . . . 14
84 addcl 9077 . . . . . . . . . . . . . . 15
8584ad2ant2lr 730 . . . . . . . . . . . . . 14
8683, 85jca 520 . . . . . . . . . . . . 13
87863adant3 978 . . . . . . . . . . . 12
88 addcom 9257 . . . . . . . . . . . 12
8987, 88syl 16 . . . . . . . . . . 11
9076, 81, 893eqtrd 2474 . . . . . . . . . 10
9167, 69, 903eqtr3rd 2479 . . . . . . . . 9
92 pire 20377 . . . . . . . . . . . 12
9392recni 9107 . . . . . . . . . . 11
94 addcom 9257 . . . . . . . . . . 11
9593, 29, 94sylancr 646 . . . . . . . . . 10
96953adant3 978 . . . . . . . . 9
9791, 96eqtrd 2470 . . . . . . . 8
9897fveq2d 5735 . . . . . . 7
99 cosppi 20403 . . . . . . . . 9
10029, 99syl 16 . . . . . . . 8
1011003adant3 978 . . . . . . 7
10298, 101eqtrd 2470 . . . . . 6
10362, 102oveq12d 6102 . . . . 5
104 subcl 9310 . . . . . . . . . 10
105104ancoms 441 . . . . . . . . 9
106105adantr 453 . . . . . . . 8
107106coscld 12737 . . . . . . 7
108107, 30subnegd 9423 . . . . . 6
1091083adant3 978 . . . . 5
110103, 109eqtrd 2470 . . . 4
111110oveq1d 6099 . . 3
112 sinmul 12778 . . . . 5
11385, 83, 112syl2anc 644 . . . 4