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 ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ∧ ( ( 𝐴 + 𝐵 ) + ( 𝐶 + 𝐷 ) ) = π ) → ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐶 ) · ( sin ‘ 𝐷 ) ) ) = ( ( sin ‘ ( 𝐵 + 𝐶 ) ) · ( sin ‘ ( 𝐴 + 𝐶 ) ) ) )

Proof

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