Theorem subsin

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

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

Proof

Step	Hyp	Ref	Expression
1		halfaddsubcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) )
2		coscl	⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ → ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
3		sincl	⊢ ( ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ → ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
4		mulcl	⊢ ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ ∧ ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
5	2 3 4	syl2an	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
6	1 5	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
7	6	2timesd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
8		sinadd	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
9		sinsub	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) = ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
10	8 9	oveq12d	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) )
11	1 10	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) )
12		sincl	⊢ ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ → ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
13		coscl	⊢ ( ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ → ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ )
14		mulcl	⊢ ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ ∧ ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
15	12 13 14	syl2an	⊢ ( ( ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℂ ∧ ( ( 𝐴 − 𝐵 ) / 2 ) ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
16	1 15	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ∈ ℂ )
17	16 6 6	pnncand	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) − ( ( ( sin ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( cos ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) ) = ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )
18	11 17	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) + ( ( 𝐴 − 𝐵 ) / 2 ) ) ) − ( sin ‘ ( ( ( 𝐴 + 𝐵 ) / 2 ) − ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) = ( ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) + ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 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	7 18 24	3eqtr2rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) − ( sin ‘ 𝐵 ) ) = ( 2 · ( ( cos ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) · ( sin ‘ ( ( 𝐴 − 𝐵 ) / 2 ) ) ) ) )