Metamath Proof Explorer

Theorem subcos

Description: Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007) (Revised by Mario Carneiro, 10-May-2014)

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

Proof

Step Hyp Ref Expression
1 halfaddsubcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ
2 sincl ⊢ A + B 2 ∈ ℂ → sin ⁡ A + B 2 ∈ ℂ
3 sincl ⊢ A − B 2 ∈ ℂ → sin ⁡ A − B 2 ∈ ℂ
4 mulcl ⊢ sin ⁡ A + B 2 ∈ ℂ ∧ sin ⁡ A − B 2 ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
5 2 3 4 syl2an ⊢ A + B 2 ∈ ℂ ∧ A − B 2 ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
6 1 5 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
7 6 2timesd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 = sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
8 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
9 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
10 8 9 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
11 1 10 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
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 1 15 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 ⁢ cos ⁡ A − B 2 ∈ ℂ
17 16 6 6 pnncand ⊢ 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 = sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
18 11 17 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 − cos ⁡ A + B 2 + A − B 2 = sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2
19 halfaddsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A ∧ A + B 2 − A − B 2 = B
20 19 simprd ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 − A − B 2 = B
21 20 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 = cos ⁡ B
22 19 simpld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 + A − B 2 = A
23 22 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 + A − B 2 = cos ⁡ A
24 21 23 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 − A − B 2 − cos ⁡ A + B 2 + A − B 2 = cos ⁡ B − cos ⁡ A
25 7 18 24 3eqtr2rd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ B − cos ⁡ A = 2 ⁢ sin ⁡ A + B 2 ⁢ sin ⁡ A − B 2