Metamath Proof Explorer

Theorem subcos

Description: Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007) (Revised by Mario Carneiro, 10-May-2014)

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

Proof

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