Metamath Proof Explorer

Theorem tanneg

Description: The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014)

Ref Expression
Assertion tanneg 
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )

Proof

Step Hyp Ref Expression
1 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
2 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
3 divneg 
 |-  ( ( ( sin ` A ) e. CC /\ ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( ( sin ` A ) / ( cos ` A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
4 2 3 syl3an1 
 |-  ( ( A e. CC /\ ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( ( sin ` A ) / ( cos ` A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
5 1 4 syl3an2 
 |-  ( ( A e. CC /\ A e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( ( sin ` A ) / ( cos ` A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
6 5 3anidm12 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( ( sin ` A ) / ( cos ` A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
7 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
8 7 negeqd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( tan ` A ) = -u ( ( sin ` A ) / ( cos ` A ) ) )
9 negcl 
 |-  ( A e. CC -> -u A e. CC )
10 cosneg 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
11 10 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` -u A ) = ( cos ` A ) )
12 simpr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) =/= 0 )
13 11 12 eqnetrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` -u A ) =/= 0 )
14 tanval 
 |-  ( ( -u A e. CC /\ ( cos ` -u A ) =/= 0 ) -> ( tan ` -u A ) = ( ( sin ` -u A ) / ( cos ` -u A ) ) )
15 9 13 14 syl2an2r 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` -u A ) = ( ( sin ` -u A ) / ( cos ` -u A ) ) )
16 sinneg 
 |-  ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
17 16 10 oveq12d 
 |-  ( A e. CC -> ( ( sin ` -u A ) / ( cos ` -u A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
18 17 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sin ` -u A ) / ( cos ` -u A ) ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
19 15 18 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` -u A ) = ( -u ( sin ` A ) / ( cos ` A ) ) )
20 6 8 19 3eqtr4rd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )