Metamath Proof Explorer

Theorem cosmul

Description: Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd and cossub . (Contributed by David A. Wheeler, 26-May-2015)

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

Proof

Step Hyp Ref Expression
1 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
2 coscl ⊢ ( 𝐵 ∈ ℂ → ( cos ‘ 𝐵 ) ∈ ℂ )
3 mulcl ⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( cos ‘ 𝐵 ) ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ )
5 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
6 3anass ⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) ↔ ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) )
7 4 5 6 sylanblrc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
8 divcan3 ⊢ ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) / 2 ) = ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
9 7 8 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) / 2 ) = ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) )
10 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
11 sincl ⊢ ( 𝐵 ∈ ℂ → ( sin ‘ 𝐵 ) ∈ ℂ )
12 mulcl ⊢ ( ( ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐵 ) ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
13 10 11 12 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ∈ ℂ )
14 4 13 4 ppncand ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
15 cossub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 − 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
16 cosadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )
17 15 16 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ ( 𝐴 − 𝐵 ) ) + ( cos ‘ ( 𝐴 + 𝐵 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) + ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) ) )
18 4 2timesd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) )
19 14 17 18 3eqtr4rd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 2 · ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) = ( ( cos ‘ ( 𝐴 − 𝐵 ) ) + ( cos ‘ ( 𝐴 + 𝐵 ) ) ) )
20 19 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 2 · ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) ) / 2 ) = ( ( ( cos ‘ ( 𝐴 − 𝐵 ) ) + ( cos ‘ ( 𝐴 + 𝐵 ) ) ) / 2 ) )
21 9 20 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) = ( ( ( cos ‘ ( 𝐴 − 𝐵 ) ) + ( cos ‘ ( 𝐴 + 𝐵 ) ) ) / 2 ) )