This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) /\ ( ( A + B ) + ( C + D ) ) = _pi ) -> ( ( ( sin ` A ) x. ( sin ` B ) ) + ( ( sin ` C ) x. ( sin ` D ) ) ) = ( ( sin ` ( B + C ) ) x. ( sin ` ( A + C ) ) ) )

Proof

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