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+B2⁢cos⁡A−B2

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+B2+A−B2=A∧A+B2−A−B2=B
6 5 simprd ⊢A∈ℂ∧B∈ℂ→A+B2−A−B2=B
7 6 fveq2d ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2−A−B2=cos⁡B
8 5 simpld ⊢A∈ℂ∧B∈ℂ→A+B2+A−B2=A
9 8 fveq2d ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2+A−B2=cos⁡A
10 7 9 oveq12d ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2−A−B2+cos⁡A+B2+A−B2=cos⁡B+cos⁡A
11 halfaddsubcl ⊢A∈ℂ∧B∈ℂ→A+B2∈ℂ∧A−B2∈ℂ
12 coscl ⊢A+B2∈ℂ→cos⁡A+B2∈ℂ
13 coscl ⊢A−B2∈ℂ→cos⁡A−B2∈ℂ
14 mulcl ⊢cos⁡A+B2∈ℂ∧cos⁡A−B2∈ℂ→cos⁡A+B2⁢cos⁡A−B2∈ℂ
15 12 13 14 syl2an ⊢A+B2∈ℂ∧A−B2∈ℂ→cos⁡A+B2⁢cos⁡A−B2∈ℂ
16 11 15 syl ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2⁢cos⁡A−B2∈ℂ
17 sincl ⊢A+B2∈ℂ→sin⁡A+B2∈ℂ
18 sincl ⊢A−B2∈ℂ→sin⁡A−B2∈ℂ
19 mulcl ⊢sin⁡A+B2∈ℂ∧sin⁡A−B2∈ℂ→sin⁡A+B2⁢sin⁡A−B2∈ℂ
20 17 18 19 syl2an ⊢A+B2∈ℂ∧A−B2∈ℂ→sin⁡A+B2⁢sin⁡A−B2∈ℂ
21 11 20 syl ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2⁢sin⁡A−B2∈ℂ
22 16 21 16 ppncand ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢sin⁡A−B2+cos⁡A+B2⁢cos⁡A−B2−sin⁡A+B2⁢sin⁡A−B2=cos⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢cos⁡A−B2
23 cossub ⊢A+B2∈ℂ∧A−B2∈ℂ→cos⁡A+B2−A−B2=cos⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢sin⁡A−B2
24 cosadd ⊢A+B2∈ℂ∧A−B2∈ℂ→cos⁡A+B2+A−B2=cos⁡A+B2⁢cos⁡A−B2−sin⁡A+B2⁢sin⁡A−B2
25 23 24 oveq12d ⊢A+B2∈ℂ∧A−B2∈ℂ→cos⁡A+B2−A−B2+cos⁡A+B2+A−B2=cos⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢sin⁡A−B2+cos⁡A+B2⁢cos⁡A−B2−sin⁡A+B2⁢sin⁡A−B2
26 11 25 syl ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2−A−B2+cos⁡A+B2+A−B2=cos⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢sin⁡A−B2+cos⁡A+B2⁢cos⁡A−B2−sin⁡A+B2⁢sin⁡A−B2
27 16 2timesd ⊢A∈ℂ∧B∈ℂ→2⁢cos⁡A+B2⁢cos⁡A−B2=cos⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢cos⁡A−B2
28 22 26 27 3eqtr4d ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2−A−B2+cos⁡A+B2+A−B2=2⁢cos⁡A+B2⁢cos⁡A−B2
29 4 10 28 3eqtr2d ⊢A∈ℂ∧B∈ℂ→cos⁡A+cos⁡B=2⁢cos⁡A+B2⁢cos⁡A−B2