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 + B 2

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 ⁡ B 2 = cos ⁡ A ⁢ cos ⁡ B
9 7 8 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ cos ⁡ A ⁢ cos ⁡ B 2 = 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 ⁡ B 2 = cos ⁡ A − B + cos ⁡ A + B 2
21 9 20 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ B = cos ⁡ A − B + cos ⁡ A + B 2