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 − B 2

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 ffvelrnda ⊢ 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 ffvelrnda ⊢ 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 − B 2 = 2 ⁢ sin ⁡ A ⁢ cos ⁡ B 2
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 ⁡ B 2 = sin ⁡ A ⁢ cos ⁡ B
23 18 22 eqtr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → sin ⁡ A ⁢ cos ⁡ B = sin ⁡ A + B + sin ⁡ A − B 2