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 ‘ ( 𝐴 + 𝐶 ) ) ) )