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		addlid	⊢ ( ( 𝐶 + 𝐷 ) ∈ ℂ → ( 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 ‘ ( 𝐴 + 𝐶 ) ) ) )