Metamath Proof Explorer

Theorem sinmulcos

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

Ref Expression
Assertion sinmulcos ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( ( sin ‘ ( 𝐴 + 𝐵 ) ) + ( sin ‘ ( 𝐴 − 𝐵 ) ) ) / 2 ) )

Proof

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