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

Proof

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