Metamath Proof Explorer

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 ) )