Metamath Proof Explorer

Theorem cossub

Description: Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 negcl 
 |-  ( B e. CC -> -u B e. CC )
2 cosadd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( cos ` ( A + -u B ) ) = ( ( ( cos ` A ) x. ( cos ` -u B ) ) - ( ( sin ` A ) x. ( sin ` -u B ) ) ) )
3 1 2 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + -u B ) ) = ( ( ( cos ` A ) x. ( cos ` -u B ) ) - ( ( sin ` A ) x. ( sin ` -u B ) ) ) )
4 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
5 4 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + -u B ) ) = ( cos ` ( A - B ) ) )
6 cosneg 
 |-  ( B e. CC -> ( cos ` -u B ) = ( cos ` B ) )
7 6 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` -u B ) = ( cos ` B ) )
8 7 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` -u B ) ) = ( ( cos ` A ) x. ( cos ` B ) ) )
9 sinneg 
 |-  ( B e. CC -> ( sin ` -u B ) = -u ( sin ` B ) )
10 9 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( sin ` -u B ) = -u ( sin ` B ) )
11 10 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` -u B ) ) = ( ( sin ` A ) x. -u ( sin ` B ) ) )
12 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
13 sincl 
 |-  ( B e. CC -> ( sin ` B ) e. CC )
14 mulneg2 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( sin ` A ) x. -u ( sin ` B ) ) = -u ( ( sin ` A ) x. ( sin ` B ) ) )
15 12 13 14 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. -u ( sin ` B ) ) = -u ( ( sin ` A ) x. ( sin ` B ) ) )
16 11 15 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` -u B ) ) = -u ( ( sin ` A ) x. ( sin ` B ) ) )
17 8 16 oveq12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` -u B ) ) - ( ( sin ` A ) x. ( sin ` -u B ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - -u ( ( sin ` A ) x. ( sin ` B ) ) ) )
18 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
19 coscl 
 |-  ( B e. CC -> ( cos ` B ) e. CC )
20 mulcl 
 |-  ( ( ( cos ` A ) e. CC /\ ( cos ` B ) e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
21 18 19 20 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) e. CC )
22 mulcl 
 |-  ( ( ( sin ` A ) e. CC /\ ( sin ` B ) e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
23 12 13 22 syl2an 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) e. CC )
24 21 23 subnegd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` B ) ) - -u ( ( sin ` A ) x. ( sin ` B ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
25 17 24 eqtrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( ( cos ` A ) x. ( cos ` -u B ) ) - ( ( sin ` A ) x. ( sin ` -u B ) ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
26 3 5 25 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A - B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )