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 ) )