Metamath Proof Explorer

Theorem cosmul

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

Ref Expression
Assertion cosmul ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢cos⁡B=cos⁡A−B+cos⁡A+B2

Proof

Step Hyp Ref Expression
1 coscl ⊢A∈ℂ→cos⁡A∈ℂ
2 coscl ⊢B∈ℂ→cos⁡B∈ℂ
3 mulcl ⊢cos⁡A∈ℂ∧cos⁡B∈ℂ→cos⁡A⁢cos⁡B∈ℂ
4 1 2 3 syl2an ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢cos⁡B∈ℂ
5 2cnne0 ⊢2∈ℂ∧2≠0
6 3anass ⊢cos⁡A⁢cos⁡B∈ℂ∧2∈ℂ∧2≠0↔cos⁡A⁢cos⁡B∈ℂ∧2∈ℂ∧2≠0
7 4 5 6 sylanblrc ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢cos⁡B∈ℂ∧2∈ℂ∧2≠0
8 divcan3 ⊢cos⁡A⁢cos⁡B∈ℂ∧2∈ℂ∧2≠0→2⁢cos⁡A⁢cos⁡B2=cos⁡A⁢cos⁡B
9 7 8 syl ⊢A∈ℂ∧B∈ℂ→2⁢cos⁡A⁢cos⁡B2=cos⁡A⁢cos⁡B
10 sincl ⊢A∈ℂ→sin⁡A∈ℂ
11 sincl ⊢B∈ℂ→sin⁡B∈ℂ
12 mulcl ⊢sin⁡A∈ℂ∧sin⁡B∈ℂ→sin⁡A⁢sin⁡B∈ℂ
13 10 11 12 syl2an ⊢A∈ℂ∧B∈ℂ→sin⁡A⁢sin⁡B∈ℂ
14 4 13 4 ppncand ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢cos⁡B+sin⁡A⁢sin⁡B+cos⁡A⁢cos⁡B−sin⁡A⁢sin⁡B=cos⁡A⁢cos⁡B+cos⁡A⁢cos⁡B
15 cossub ⊢A∈ℂ∧B∈ℂ→cos⁡A−B=cos⁡A⁢cos⁡B+sin⁡A⁢sin⁡B
16 cosadd ⊢A∈ℂ∧B∈ℂ→cos⁡A+B=cos⁡A⁢cos⁡B−sin⁡A⁢sin⁡B
17 15 16 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
18 4 2timesd ⊢A∈ℂ∧B∈ℂ→2⁢cos⁡A⁢cos⁡B=cos⁡A⁢cos⁡B+cos⁡A⁢cos⁡B
19 14 17 18 3eqtr4rd ⊢A∈ℂ∧B∈ℂ→2⁢cos⁡A⁢cos⁡B=cos⁡A−B+cos⁡A+B
20 19 oveq1d ⊢A∈ℂ∧B∈ℂ→2⁢cos⁡A⁢cos⁡B2=cos⁡A−B+cos⁡A+B2
21 9 20 eqtr3d ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢cos⁡B=cos⁡A−B+cos⁡A+B2