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 ⊢A∈ℂ∧B∈ℂ→sin⁡A⁢sin⁡B=cos⁡A−B−cos⁡A+B2

Proof

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