Metamath Proof Explorer

Theorem addcos

Description: Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 coscl ⊢ A ∈ ℂ → cos ⁡ A ∈ ℂ
2 coscl ⊢ B ∈ ℂ → cos ⁡ B ∈ ℂ
3 addcom ⊢ cos ⁡ A ∈ ℂ ∧ cos ⁡ B ∈ ℂ → cos ⁡ A + cos ⁡ B = cos ⁡ B + cos ⁡ A
4 1 2 3 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + cos ⁡ B = cos ⁡ B + cos ⁡ A
5 halfaddsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A ∧ A + B 2 − A − B 2 = B
6 5 simprd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 − A − B 2 = B
7 6 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 = cos ⁡ B
8 5 simpld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A
9 8 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 + A − B 2 = cos ⁡ A
10 7 9 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 + cos ⁡ A + B 2 + A − B 2 = cos ⁡ B + cos ⁡ A
11 halfaddsubcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ
12 coscl ⊢ A + B 2 ∈ ℂ → cos ⁡ A + B 2 ∈ ℂ
13 coscl ⊢ A − B 2 ∈ ℂ → cos ⁡ A − B 2 ∈ ℂ
14 mulcl ⊢ cos ⁡ A + B 2 ∈ ℂ ∧ cos ⁡ A − B 2 ∈ ℂ → cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 ∈ ℂ
15 12 13 14 syl2an ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 ∈ ℂ
16 11 15 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 ∈ ℂ
17 sincl ⊢ A + B 2 ∈ ℂ → sin ⁡ A + B 2 ∈ ℂ
18 sincl ⊢ A − B 2 ∈ ℂ → sin ⁡ A − B 2 ∈ ℂ
19 mulcl ⊢ sin ⁡ A + B 2 ∈ ℂ ∧ sin ⁡ A − B 2 ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
20 17 18 19 syl2an ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
21 11 20 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
22 16 21 16 ppncand ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 − sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2
23 cossub ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → cos ⁡ A + B 2 − A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
24 cosadd ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → cos ⁡ A + B 2 + A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 − sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
25 23 24 oveq12d ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → cos ⁡ A + B 2 − A − B 2 + cos ⁡ A + B 2 + A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 − sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
26 11 25 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 + cos ⁡ A + B 2 + A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 − sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
27 16 2timesd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 = cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2
28 22 26 27 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 + cos ⁡ A + B 2 + A − B 2 = 2 ⁢ cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2
29 4 10 28 3eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + cos ⁡ B = 2 ⁢ cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2