Metamath Proof Explorer

Theorem subsin

Description: Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007)

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

Proof

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