Metamath Proof Explorer

Theorem addsin

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

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

Proof

Step Hyp Ref Expression
1 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
2 1 halfcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B 2 ∈ ℂ
3 2 sincld ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 ∈ ℂ
4 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
5 4 halfcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B 2 ∈ ℂ
6 5 coscld ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A − B 2 ∈ ℂ
7 3 6 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 ∈ ℂ
8 7 2timesd ⊢ A ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 = sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2
9 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
10 2 5 9 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 + A − B 2 = sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + cos ⁡ A + B 2 ⁢ sin ⁡ A − B 2
11 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
12 2 5 11 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 − A − B 2 = sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 − cos ⁡ A + B 2 ⁢ sin ⁡ A − B 2
13 10 12 oveq12d ⊢ 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
14 2 coscld ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 ∈ ℂ
15 5 sincld ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A − B 2 ∈ ℂ
16 14 15 mulcld ⊢ A ∈ ℂ ∧ B ∈ ℂ → cos ⁡ A + B 2 ⁢ sin ⁡ A − B 2 ∈ ℂ
17 7 16 7 ppncand ⊢ 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 = sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2
18 13 17 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + B 2 + A − B 2 + sin ⁡ A + B 2 − A − B 2 = sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2 + sin ⁡ A + B 2 ⁢ cos ⁡ 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 8 18 24 3eqtr2rd ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A + sin ⁡ B = 2 ⁢ sin ⁡ A + B 2 ⁢ cos ⁡ A − B 2