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 
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
2 coscl 
 |-  ( B e. CC -> ( cos ` B ) e. CC )
3 mulcl 
 |-  ( ( ( cos ` A ) e. CC /\ ( cos ` B ) e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
4 1 2 3 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
5 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
6 3anass 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) <-> ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) )
7 4 5 6 sylanblrc 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) )
8 divcan3 
 |-  ( ( ( ( cos ` A ) x. ( cos ` B ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. ( ( cos ` A ) x. ( cos ` B ) ) ) / 2 ) = ( ( cos ` A ) x. ( cos ` B ) ) )
9 7 8 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. ( ( cos ` A ) x. ( cos ` B ) ) ) / 2 ) = ( ( cos ` A ) x. ( cos ` B ) ) )
10 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
11 sincl 
 |-  ( B e. CC -> ( sin ` B ) e. CC )
12 mulcl 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
13 10 11 12 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
14 4 13 4 ppncand 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) + ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( cos ` B ) ) ) )
15 cossub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A - B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
16 cosadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
17 15 16 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) = ( ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) + ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) ) )
18 4 2timesd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( cos ` A ) x. ( cos ` B ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( cos ` B ) ) ) )
19 14 17 18 3eqtr4rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( cos ` A ) x. ( cos ` B ) ) ) = ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) )
20 19 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. ( ( cos ` A ) x. ( cos ` B ) ) ) / 2 ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )
21 9 20 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )