Metamath Proof Explorer


Theorem ptolemy

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 , 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)

Ref Expression
Assertion ptolemy A B C D A + B + C + D = π sin A sin B + sin C sin D = sin B + C sin A + C

Proof

Step Hyp Ref Expression
1 addcl C D C + D
2 1 3ad2ant2 A B C D A + B + C + D = π C + D
3 2 coscld A B C D A + B + C + D = π cos C + D
4 3 negnegd A B C D A + B + C + D = π cos C + D = cos C + D
5 addid2 C + D 0 + C + D = C + D
6 5 oveq1d C + D 0 + C + D - A + B + C + D = C + D - A + B + C + D
7 2 6 syl A B C D A + B + C + D = π 0 + C + D - A + B + C + D = C + D - A + B + C + D
8 0cnd A B C D A + B + C + D = π 0
9 addcl A B A + B
10 9 adantr A B C D A + B
11 10 3adant3 A B C D A + B + C + D = π A + B
12 8 11 2 pnpcan2d A B C D A + B + C + D = π 0 + C + D - A + B + C + D = 0 A + B
13 simp3 A B C D A + B + C + D = π A + B + C + D = π
14 13 oveq2d A B C D A + B + C + D = π C + D - A + B + C + D = C + D - π
15 7 12 14 3eqtr3rd A B C D A + B + C + D = π C + D - π = 0 A + B
16 df-neg A + B = 0 A + B
17 15 16 eqtr4di A B C D A + B + C + D = π C + D - π = A + B
18 17 fveq2d A B C D A + B + C + D = π cos C + D - π = cos A + B
19 cosmpi C + D cos C + D - π = cos C + D
20 2 19 syl A B C D A + B + C + D = π cos C + D - π = cos C + D
21 cosneg A + B cos A + B = cos A + B
22 11 21 syl A B C D A + B + C + D = π cos A + B = cos A + B
23 18 20 22 3eqtr3d A B C D A + B + C + D = π cos C + D = cos A + B
24 23 negeqd A B C D A + B + C + D = π cos C + D = cos A + B
25 4 24 eqtr3d A B C D A + B + C + D = π cos C + D = cos A + B
26 25 oveq2d A B C D A + B + C + D = π cos C D cos C + D = cos C D cos A + B
27 subcl C D C D
28 27 adantl A B C D C D
29 28 coscld A B C D cos C D
30 29 3adant3 A B C D A + B + C + D = π cos C D
31 11 coscld A B C D A + B + C + D = π cos A + B
32 30 31 subnegd A B C D A + B + C + D = π cos C D cos A + B = cos C D + cos A + B
33 26 32 eqtrd A B C D A + B + C + D = π cos C D cos C + D = cos C D + cos A + B
34 33 oveq1d A B C D A + B + C + D = π cos C D cos C + D 2 = cos C D + cos A + B 2
35 34 oveq2d A B C D A + B + C + D = π cos A B cos A + B 2 + cos C D cos C + D 2 = cos A B cos A + B 2 + cos C D + cos A + B 2
36 subcl A B A B
37 36 3ad2ant1 A B C D A + B + C + D = π A B
38 37 coscld A B C D A + B + C + D = π cos A B
39 38 31 subcld A B C D A + B + C + D = π cos A B cos A + B
40 30 31 addcld A B C D A + B + C + D = π cos C D + cos A + B
41 2cnne0 2 2 0
42 41 a1i A B C D A + B + C + D = π 2 2 0
43 divdir cos A B cos A + B cos C D + cos A + B 2 2 0 cos A B cos A + B + cos C D + cos A + B 2 = cos A B cos A + B 2 + cos C D + cos A + B 2
44 39 40 42 43 syl3anc A B C D A + B + C + D = π cos A B cos A + B + cos C D + cos A + B 2 = cos A B cos A + B 2 + cos C D + cos A + B 2
45 38 31 30 nppcan3d A B C D A + B + C + D = π cos A B cos A + B + cos C D + cos A + B = cos A B + cos C D
46 45 oveq1d A B C D A + B + C + D = π cos A B cos A + B + cos C D + cos A + B 2 = cos A B + cos C D 2
47 44 46 eqtr3d A B C D A + B + C + D = π cos A B cos A + B 2 + cos C D + cos A + B 2 = cos A B + cos C D 2
48 35 47 eqtrd A B C D A + B + C + D = π cos A B cos A + B 2 + cos C D cos C + D 2 = cos A B + cos C D 2
49 sinmul A B sin A sin B = cos A B cos A + B 2
50 49 3ad2ant1 A B C D A + B + C + D = π sin A sin B = cos A B cos A + B 2
51 sinmul C D sin C sin D = cos C D cos C + D 2
52 51 3ad2ant2 A B C D A + B + C + D = π sin C sin D = cos C D cos C + D 2
53 50 52 oveq12d A B C D A + B + C + D = π sin A sin B + sin C sin D = cos A B cos A + B 2 + cos C D cos C + D 2
54 simplr A B C D B
55 simpll A B C D A
56 simprl A B C D C
57 54 55 56 pnpcan2d A B C D B + C - A + C = B A
58 57 fveq2d A B C D cos B + C - A + C = cos B A
59 58 3adant3 A B C D A + B + C + D = π cos B + C - A + C = cos B A
60 1 adantl A B C D C + D
61 10 60 28 3jca A B C D A + B C + D C D
62 61 3adant3 A B C D A + B + C + D = π A + B C + D C D
63 addass A + B C + D C D A + B + C + D + C D = A + B + C + D + C D
64 62 63 syl A B C D A + B + C + D = π A + B + C + D + C D = A + B + C + D + C D
65 oveq1 A + B + C + D = π A + B + C + D + C D = π + C - D
66 65 3ad2ant3 A B C D A + B + C + D = π A + B + C + D + C D = π + C - D
67 simpl C D C
68 simpr C D D
69 67 68 67 3jca C D C D C
70 69 3ad2ant2 A B C D A + B + C + D = π C D C
71 ppncan C D C C + D + C D = C + C
72 71 oveq2d C D C A + B + C + D + C D = A + B + C + C
73 70 72 syl A B C D A + B + C + D = π A + B + C + D + C D = A + B + C + C
74 simp1 A B C D A + B + C + D = π A B
75 67 67 jca C D C C
76 75 3ad2ant2 A B C D A + B + C + D = π C C
77 add4 A B C C A + B + C + C = A + C + B + C
78 74 76 77 syl2anc A B C D A + B + C + D = π A + B + C + C = A + C + B + C
79 addcl A C A + C
80 79 ad2ant2r A B C D A + C
81 addcl B C B + C
82 81 ad2ant2lr A B C D B + C
83 80 82 jca A B C D A + C B + C
84 83 3adant3 A B C D A + B + C + D = π A + C B + C
85 addcom A + C B + C A + C + B + C = B + C + A + C
86 84 85 syl A B C D A + B + C + D = π A + C + B + C = B + C + A + C
87 73 78 86 3eqtrd A B C D A + B + C + D = π A + B + C + D + C D = B + C + A + C
88 64 66 87 3eqtr3rd A B C D A + B + C + D = π B + C + A + C = π + C - D
89 picn π
90 addcom π C D π + C - D = C - D + π
91 89 28 90 sylancr A B C D π + C - D = C - D + π
92 91 3adant3 A B C D A + B + C + D = π π + C - D = C - D + π
93 88 92 eqtrd A B C D A + B + C + D = π B + C + A + C = C - D + π
94 93 fveq2d A B C D A + B + C + D = π cos B + C + A + C = cos C - D + π
95 cosppi C D cos C - D + π = cos C D
96 28 95 syl A B C D cos C - D + π = cos C D
97 96 3adant3 A B C D A + B + C + D = π cos C - D + π = cos C D
98 94 97 eqtrd A B C D A + B + C + D = π cos B + C + A + C = cos C D
99 59 98 oveq12d A B C D A + B + C + D = π cos B + C - A + C cos B + C + A + C = cos B A cos C D
100 subcl B A B A
101 100 ancoms A B B A
102 101 adantr A B C D B A
103 102 coscld A B C D cos B A
104 103 29 subnegd A B C D cos B A cos C D = cos B A + cos C D
105 104 3adant3 A B C D A + B + C + D = π cos B A cos C D = cos B A + cos C D
106 99 105 eqtrd A B C D A + B + C + D = π cos B + C - A + C cos B + C + A + C = cos B A + cos C D
107 106 oveq1d A B C D A + B + C + D = π cos B + C - A + C cos B + C + A + C 2 = cos B A + cos C D 2
108 sinmul B + C A + C sin B + C sin A + C = cos B + C - A + C cos B + C + A + C 2
109 82 80 108 syl2anc A B C D sin B + C sin A + C = cos B + C - A + C cos B + C + A + C 2
110 109 3adant3 A B C D A + B + C + D = π sin B + C sin A + C = cos B + C - A + C cos B + C + A + C 2
111 cosneg A B cos A B = cos A B
112 36 111 syl A B cos A B = cos A B
113 negsubdi2 A B A B = B A
114 113 fveq2d A B cos A B = cos B A
115 112 114 eqtr3d A B cos A B = cos B A
116 115 3ad2ant1 A B C D A + B + C + D = π cos A B = cos B A
117 116 oveq1d A B C D A + B + C + D = π cos A B + cos C D = cos B A + cos C D
118 117 oveq1d A B C D A + B + C + D = π cos A B + cos C D 2 = cos B A + cos C D 2
119 107 110 118 3eqtr4d A B C D A + B + C + D = π sin B + C sin A + C = cos A B + cos C D 2
120 48 53 119 3eqtr4d A B C D A + B + C + D = π sin A sin B + sin C sin D = sin B + C sin A + C