Theorem addsin

Description: Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007)

	Ref	Expression
Assertion	addsin	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) + ( sin ‘ 𝐵 ) ) = ( 2 · ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
2	1	halfcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ )
3	2	sincld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
4		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 − 𝐵 ) ∈ ℂ )
5	4	halfcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ )
6	5	coscld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
7	3 6	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
8	7	2timesd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
9		sinadd	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
10	2 5 9	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
11		sinsub	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
12	2 5 11	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
13	10 12	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) + ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) )
14	2	coscld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
15	5	sincld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
16	14 15	mulcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
17	7 16 7	ppncand	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) + ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
18	13 17	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
19		halfaddsub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐴 ∧ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐵 ) )
20	19	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐴 )
21	20	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( sin ‘ 𝐴 ) )
22	19	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) = 𝐵 )
23	22	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( sin ‘ 𝐵 ) )
24	21 23	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( sin ‘ 𝐴 ) + ( sin ‘ 𝐵 ) ) )
25	8 18 24	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) + ( sin ‘ 𝐵 ) ) = ( 2 · ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )