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+B2⁢cos⁡A−B2

Proof

Step Hyp Ref Expression
1 addcl ⊢A∈ℂ∧B∈ℂ→A+B∈ℂ
2 1 halfcld ⊢A∈ℂ∧B∈ℂ→A+B2∈ℂ
3 2 sincld ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2∈ℂ
4 subcl ⊢A∈ℂ∧B∈ℂ→A−B∈ℂ
5 4 halfcld ⊢A∈ℂ∧B∈ℂ→A−B2∈ℂ
6 5 coscld ⊢A∈ℂ∧B∈ℂ→cos⁡A−B2∈ℂ
7 3 6 mulcld ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2⁢cos⁡A−B2∈ℂ
8 7 2timesd ⊢A∈ℂ∧B∈ℂ→2⁢sin⁡A+B2⁢cos⁡A−B2=sin⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢cos⁡A−B2
9 sinadd ⊢A+B2∈ℂ∧A−B2∈ℂ→sin⁡A+B2+A−B2=sin⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢sin⁡A−B2
10 2 5 9 syl2anc ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2+A−B2=sin⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢sin⁡A−B2
11 sinsub ⊢A+B2∈ℂ∧A−B2∈ℂ→sin⁡A+B2−A−B2=sin⁡A+B2⁢cos⁡A−B2−cos⁡A+B2⁢sin⁡A−B2
12 2 5 11 syl2anc ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2−A−B2=sin⁡A+B2⁢cos⁡A−B2−cos⁡A+B2⁢sin⁡A−B2
13 10 12 oveq12d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2+A−B2+sin⁡A+B2−A−B2=sin⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢sin⁡A−B2+sin⁡A+B2⁢cos⁡A−B2−cos⁡A+B2⁢sin⁡A−B2
14 2 coscld ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2∈ℂ
15 5 sincld ⊢A∈ℂ∧B∈ℂ→sin⁡A−B2∈ℂ
16 14 15 mulcld ⊢A∈ℂ∧B∈ℂ→cos⁡A+B2⁢sin⁡A−B2∈ℂ
17 7 16 7 ppncand ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2⁢cos⁡A−B2+cos⁡A+B2⁢sin⁡A−B2+sin⁡A+B2⁢cos⁡A−B2−cos⁡A+B2⁢sin⁡A−B2=sin⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢cos⁡A−B2
18 13 17 eqtrd ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2+A−B2+sin⁡A+B2−A−B2=sin⁡A+B2⁢cos⁡A−B2+sin⁡A+B2⁢cos⁡A−B2
19 halfaddsub ⊢A∈ℂ∧B∈ℂ→A+B2+A−B2=A∧A+B2−A−B2=B
20 19 simpld ⊢A∈ℂ∧B∈ℂ→A+B2+A−B2=A
21 20 fveq2d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2+A−B2=sin⁡A
22 19 simprd ⊢A∈ℂ∧B∈ℂ→A+B2−A−B2=B
23 22 fveq2d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2−A−B2=sin⁡B
24 21 23 oveq12d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B2+A−B2+sin⁡A+B2−A−B2=sin⁡A+sin⁡B
25 8 18 24 3eqtr2rd ⊢A∈ℂ∧B∈ℂ→sin⁡A+sin⁡B=2⁢sin⁡A+B2⁢cos⁡A−B2