Theorem sinmul

Description: Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd and cossub . (Contributed by David A. Wheeler, 26-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cossub	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 − 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
2		cosadd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
3	1 2	oveq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( 𝐴 − 𝐵 ) ) − ( cos ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) )
4		coscl	⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
5		coscl	⊢ ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
6		mulcl	⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐵 ) ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
7	4 5 6	syl2an	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
8		sincl	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
9		sincl	⊢ ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
10		mulcl	⊢ ( ( ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
11	8 9 10	syl2an	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
12		pnncan	⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
13	12	3anidm23	⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
14		2times	⊢ ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ → ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
15	14	adantl	⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ) → ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
16	13 15	eqtr4d	⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
17	7 11 16	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) − ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
18		2cn	⊢ 2 ∈ ℂ
19		mulcom	⊢ ( ( 2 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ) → ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) )
20	18 11 19	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) )
21	3 17 20	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( 𝐴 − 𝐵 ) ) − ( cos ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) )
22	21	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ ( 𝐴 − 𝐵 ) ) − ( cos ‘ ( 𝐴 + 𝐵 ) ) ) / 2 ) = ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) / 2 ) )
23		2ne0	⊢ 2 ≠ 0
24		divcan4	⊢ ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) / 2 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
25	18 23 24	mp3an23	⊢ ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ → ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) / 2 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
26	11 25	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) · 2 ) / 2 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) )
27	22 26	eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) = ( ( ( cos ‘ ( 𝐴 − 𝐵 ) ) − ( cos ‘ ( 𝐴 + 𝐵 ) ) ) / 2 ) )