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