Metamath Proof Explorer

Theorem sinmulcos

Description: Multiplication formula for sine and cosine. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 simpl ⊢A∈ℂ∧B∈ℂ→A∈ℂ
2 1 sincld ⊢A∈ℂ∧B∈ℂ→sin⁡A∈ℂ
3 cosf ⊢cos:ℂ⟶ℂ
4 3 a1i ⊢A∈ℂ→cos:ℂ⟶ℂ
5 4 ffvelcdmda ⊢A∈ℂ∧B∈ℂ→cos⁡B∈ℂ
6 2 5 mulcld ⊢A∈ℂ∧B∈ℂ→sin⁡A⁢cos⁡B∈ℂ
7 1 coscld ⊢A∈ℂ∧B∈ℂ→cos⁡A∈ℂ
8 sinf ⊢sin:ℂ⟶ℂ
9 8 a1i ⊢A∈ℂ→sin:ℂ⟶ℂ
10 9 ffvelcdmda ⊢A∈ℂ∧B∈ℂ→sin⁡B∈ℂ
11 7 10 mulcld ⊢A∈ℂ∧B∈ℂ→cos⁡A⁢sin⁡B∈ℂ
12 6 11 6 ppncand ⊢A∈ℂ∧B∈ℂ→sin⁡A⁢cos⁡B+cos⁡A⁢sin⁡B+sin⁡A⁢cos⁡B−cos⁡A⁢sin⁡B=sin⁡A⁢cos⁡B+sin⁡A⁢cos⁡B
13 sinadd ⊢A∈ℂ∧B∈ℂ→sin⁡A+B=sin⁡A⁢cos⁡B+cos⁡A⁢sin⁡B
14 sinsub ⊢A∈ℂ∧B∈ℂ→sin⁡A−B=sin⁡A⁢cos⁡B−cos⁡A⁢sin⁡B
15 13 14 oveq12d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B+sin⁡A−B=sin⁡A⁢cos⁡B+cos⁡A⁢sin⁡B+sin⁡A⁢cos⁡B−cos⁡A⁢sin⁡B
16 6 2timesd ⊢A∈ℂ∧B∈ℂ→2⁢sin⁡A⁢cos⁡B=sin⁡A⁢cos⁡B+sin⁡A⁢cos⁡B
17 12 15 16 3eqtr4d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B+sin⁡A−B=2⁢sin⁡A⁢cos⁡B
18 17 oveq1d ⊢A∈ℂ∧B∈ℂ→sin⁡A+B+sin⁡A−B2=2⁢sin⁡A⁢cos⁡B2
19 2cnd ⊢A∈ℂ∧B∈ℂ→2∈ℂ
20 2ne0 ⊢2≠0
21 20 a1i ⊢A∈ℂ∧B∈ℂ→2≠0
22 6 19 21 divcan3d ⊢A∈ℂ∧B∈ℂ→2⁢sin⁡A⁢cos⁡B2=sin⁡A⁢cos⁡B
23 18 22 eqtr2d ⊢A∈ℂ∧B∈ℂ→sin⁡A⁢cos⁡B=sin⁡A+B+sin⁡A−B2