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