Metamath Proof Explorer

Theorem cossub

Description: Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 cosadd ⊢ A ∈ ℂ ∧ − B ∈ ℂ → cos ⁡ A + − B = cos ⁡ A ⁢ cos ⁡ − B − sin ⁡ A ⁢ sin ⁡ − B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + − B = cos ⁡ A ⁢ cos ⁡ − B − sin ⁡ A ⁢ sin ⁡ − B
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 4 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + − B = cos ⁡ A − B
6 cosneg ⊢ B ∈ ℂ → cos ⁡ − B = cos ⁡ B
7 6 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ − B = cos ⁡ B
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ − B = cos ⁡ A ⁢ cos ⁡ B
9 sinneg ⊢ B ∈ ℂ → sin ⁡ − B = − sin ⁡ B
10 9 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ − B = − sin ⁡ B
11 10 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A ⁢ sin ⁡ − B = sin ⁡ A ⁢ − sin ⁡ B
12 sincl ⊢ A ∈ ℂ → sin ⁡ A ∈ ℂ
13 sincl ⊢ B ∈ ℂ → sin ⁡ B ∈ ℂ
14 mulneg2 ⊢ sin ⁡ A ∈ ℂ ∧ sin ⁡ B ∈ ℂ → sin ⁡ A ⁢ − sin ⁡ B = − sin ⁡ A ⁢ sin ⁡ B
15 12 13 14 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A ⁢ − sin ⁡ B = − sin ⁡ A ⁢ sin ⁡ B
16 11 15 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A ⁢ sin ⁡ − B = − sin ⁡ A ⁢ sin ⁡ B
17 8 16 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ − B − sin ⁡ A ⁢ sin ⁡ − B = cos ⁡ A ⁢ cos ⁡ B − − sin ⁡ A ⁢ sin ⁡ B
18 coscl ⊢ A ∈ ℂ → cos ⁡ A ∈ ℂ
19 coscl ⊢ B ∈ ℂ → cos ⁡ B ∈ ℂ
20 mulcl ⊢ cos ⁡ A ∈ ℂ ∧ cos ⁡ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ B ∈ ℂ
21 18 19 20 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ B ∈ ℂ
22 mulcl ⊢ sin ⁡ A ∈ ℂ ∧ sin ⁡ B ∈ ℂ → sin ⁡ A ⁢ sin ⁡ B ∈ ℂ
23 12 13 22 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A ⁢ sin ⁡ B ∈ ℂ
24 21 23 subnegd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ B − − sin ⁡ A ⁢ sin ⁡ B = cos ⁡ A ⁢ cos ⁡ B + sin ⁡ A ⁢ sin ⁡ B
25 17 24 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A ⁢ cos ⁡ − B − sin ⁡ A ⁢ sin ⁡ − B = cos ⁡ A ⁢ cos ⁡ B + sin ⁡ A ⁢ sin ⁡ B
26 3 5 25 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A − B = cos ⁡ A ⁢ cos ⁡ B + sin ⁡ A ⁢ sin ⁡ B