Metamath Proof Explorer

Theorem sinsub

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

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

Proof

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