Metamath Proof Explorer

Theorem sinmulcos

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

Ref Expression
Assertion sinmulcos 
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) = ( ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) / 2 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
2 1 sincld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` A ) e. CC )
3 cosf 
 |-  cos : CC --> CC
4 3 a1i 
 |-  ( A e. CC -> cos : CC --> CC )
5 4 ffvelrnda 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` B ) e. CC )
6 2 5 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) e. CC )
7 1 coscld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` A ) e. CC )
8 sinf 
 |-  sin : CC --> CC
9 8 a1i 
 |-  ( A e. CC -> sin : CC --> CC )
10 9 ffvelrnda 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` B ) e. CC )
11 7 10 mulcld 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( sin ` B ) ) e. CC )
12 6 11 6 ppncand 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( sin ` B ) ) ) + ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( cos ` B ) ) ) )
13 sinadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A + B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( sin ` B ) ) ) )
14 sinsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A - B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) )
15 13 14 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) = ( ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( sin ` B ) ) ) + ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) ) )
16 6 2timesd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 2 x. ( ( sin ` A ) x. ( cos ` B ) ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( cos ` B ) ) ) )
17 12 15 16 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` B ) ) ) )
18 17 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) / 2 ) = ( ( 2 x. ( ( sin ` A ) x. ( cos ` B ) ) ) / 2 ) )
19 2cnd 
 |-  ( ( A e. CC /\ B e. CC ) -> 2 e. CC )
20 2ne0 
 |-  2 =/= 0
21 20 a1i 
 |-  ( ( A e. CC /\ B e. CC ) -> 2 =/= 0 )
22 6 19 21 divcan3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( 2 x. ( ( sin ` A ) x. ( cos ` B ) ) ) / 2 ) = ( ( sin ` A ) x. ( cos ` B ) ) )
23 18 22 eqtr2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( cos ` B ) ) = ( ( ( sin ` ( A + B ) ) + ( sin ` ( A - B ) ) ) / 2 ) )