Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ptolemy Unicode version

Theorem ptolemy 12918
 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 11458, 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 7752 . . . . . . . . . . 11
213ad2ant2 1003 . . . . . . . . . 10
32coscld 11425 . . . . . . . . 9
43negnegd 8071 . . . . . . . 8
5 addid2 7908 . . . . . . . . . . . . . . 15
65oveq1d 5789 . . . . . . . . . . . . . 14
72, 6syl 14 . . . . . . . . . . . . 13
8 0cnd 7766 . . . . . . . . . . . . . 14
9 addcl 7752 . . . . . . . . . . . . . . . 16
109adantr 274 . . . . . . . . . . . . . . 15
11103adant3 1001 . . . . . . . . . . . . . 14
128, 11, 2pnpcan2d 8118 . . . . . . . . . . . . 13
13 simp3 983 . . . . . . . . . . . . . 14
1413oveq2d 5790 . . . . . . . . . . . . 13
157, 12, 143eqtr3rd 2181 . . . . . . . . . . . 12
16 df-neg 7943 . . . . . . . . . . . 12
1715, 16syl6eqr 2190 . . . . . . . . . . 11
1817fveq2d 5425 . . . . . . . . . 10
19 cosmpi 12910 . . . . . . . . . . 11
202, 19syl 14 . . . . . . . . . 10
21 cosneg 11441 . . . . . . . . . . 11
2211, 21syl 14 . . . . . . . . . 10
2318, 20, 223eqtr3d 2180 . . . . . . . . 9
2423negeqd 7964 . . . . . . . 8
254, 24eqtr3d 2174 . . . . . . 7
2625oveq2d 5790 . . . . . 6
27 subcl 7968 . . . . . . . . . 10
2827adantl 275 . . . . . . . . 9
2928coscld 11425 . . . . . . . 8
30293adant3 1001 . . . . . . 7
3111coscld 11425 . . . . . . 7
3230, 31subnegd 8087 . . . . . 6
3326, 32eqtrd 2172 . . . . 5
3433oveq1d 5789 . . . 4
3534oveq2d 5790 . . 3
36 subcl 7968 . . . . . . . 8
37363ad2ant1 1002 . . . . . . 7
3837coscld 11425 . . . . . 6
3938, 31subcld 8080 . . . . 5
4030, 31addcld 7792 . . . . 5
41 2cn 8798 . . . . . . 7
42 2ap0 8820 . . . . . . 7 #
4341, 42pm3.2i 270 . . . . . 6 #
4443a1i 9 . . . . 5 #
45 divdirap 8464 . . . . 5 #
4639, 40, 44, 45syl3anc 1216 . . . 4
4738, 31, 30nppcan3d 8107 . . . . 5
4847oveq1d 5789 . . . 4
4946, 48eqtr3d 2174 . . 3
5035, 49eqtrd 2172 . 2
51 sinmul 11458 . . . 4
53 sinmul 11458 . . . 4
5552, 54oveq12d 5792 . 2
56 simplr 519 . . . . . . . . 9
57 simpll 518 . . . . . . . . 9
58 simprl 520 . . . . . . . . 9
5956, 57, 58pnpcan2d 8118 . . . . . . . 8
6059fveq2d 5425 . . . . . . 7
61603adant3 1001 . . . . . 6
621adantl 275 . . . . . . . . . . . . 13
6310, 62, 283jca 1161 . . . . . . . . . . . 12
64633adant3 1001 . . . . . . . . . . 11
65 addass 7757 . . . . . . . . . . 11
6664, 65syl 14 . . . . . . . . . 10
67 oveq1 5781 . . . . . . . . . . 11
68673ad2ant3 1004 . . . . . . . . . 10
69 simpl 108 . . . . . . . . . . . . . 14
70 simpr 109 . . . . . . . . . . . . . 14
7169, 70, 693jca 1161 . . . . . . . . . . . . 13
72713ad2ant2 1003 . . . . . . . . . . . 12
73 ppncan 8011 . . . . . . . . . . . . 13
7473oveq2d 5790 . . . . . . . . . . . 12
7572, 74syl 14 . . . . . . . . . . 11
76 simp1 981 . . . . . . . . . . . 12
7769, 69jca 304 . . . . . . . . . . . . 13
78773ad2ant2 1003 . . . . . . . . . . . 12
79 add4 7930 . . . . . . . . . . . 12
8076, 78, 79syl2anc 408 . . . . . . . . . . 11
81 addcl 7752 . . . . . . . . . . . . . . 15
8281ad2ant2r 500 . . . . . . . . . . . . . 14
83 addcl 7752 . . . . . . . . . . . . . . 15
8483ad2ant2lr 501 . . . . . . . . . . . . . 14
8582, 84jca 304 . . . . . . . . . . . . 13
86853adant3 1001 . . . . . . . . . . . 12
87 addcom 7906 . . . . . . . . . . . 12
8886, 87syl 14 . . . . . . . . . . 11
8975, 80, 883eqtrd 2176 . . . . . . . . . 10
9066, 68, 893eqtr3rd 2181 . . . . . . . . 9
91 picn 12881 . . . . . . . . . . 11
92 addcom 7906 . . . . . . . . . . 11
9391, 28, 92sylancr 410 . . . . . . . . . 10
94933adant3 1001 . . . . . . . . 9
9590, 94eqtrd 2172 . . . . . . . 8
9695fveq2d 5425 . . . . . . 7
97 cosppi 12912 . . . . . . . . 9
9828, 97syl 14 . . . . . . . 8
99983adant3 1001 . . . . . . 7
10096, 99eqtrd 2172 . . . . . 6
10161, 100oveq12d 5792 . . . . 5
102 subcl 7968 . . . . . . . . . 10
103102ancoms 266 . . . . . . . . 9
104103adantr 274 . . . . . . . 8
105104coscld 11425 . . . . . . 7
106105, 29subnegd 8087 . . . . . 6
1071063adant3 1001 . . . . 5
108101, 107eqtrd 2172 . . . 4
109108oveq1d 5789 . . 3
110 sinmul 11458 . . . . 5
11184, 82, 110syl2anc 408 . . . 4