Metamath Proof Explorer

Theorem atandmtan

Description: The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandmtan 
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. dom arctan )

Proof

Step Hyp Ref Expression
1 tancl 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. CC )
2 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
3 2 oveq1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( tan ` A ) ^ 2 ) = ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) )
4 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
5 4 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sin ` A ) e. CC )
6 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
7 6 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) e. CC )
8 simpr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) =/= 0 )
9 5 7 8 sqdivd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) / ( cos ` A ) ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
10 3 9 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( tan ` A ) ^ 2 ) = ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) )
11 5 sqcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sin ` A ) ^ 2 ) e. CC )
12 7 sqcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( cos ` A ) ^ 2 ) e. CC )
13 12 negcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> -u ( ( cos ` A ) ^ 2 ) e. CC )
14 11 12 subnegd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) - -u ( ( cos ` A ) ^ 2 ) ) = ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) )
15 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
16 15 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
17 14 16 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) - -u ( ( cos ` A ) ^ 2 ) ) = 1 )
18 ax-1ne0 
 |-  1 =/= 0
19 18 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> 1 =/= 0 )
20 17 19 eqnetrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) - -u ( ( cos ` A ) ^ 2 ) ) =/= 0 )
21 11 13 20 subne0ad 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sin ` A ) ^ 2 ) =/= -u ( ( cos ` A ) ^ 2 ) )
22 12 mulm1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( -u 1 x. ( ( cos ` A ) ^ 2 ) ) = -u ( ( cos ` A ) ^ 2 ) )
23 21 22 neeqtrrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sin ` A ) ^ 2 ) =/= ( -u 1 x. ( ( cos ` A ) ^ 2 ) ) )
24 neg1cn 
 |-  -u 1 e. CC
25 24 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> -u 1 e. CC )
26 sqne0 
 |-  ( ( cos ` A ) e. CC -> ( ( ( cos ` A ) ^ 2 ) =/= 0 <-> ( cos ` A ) =/= 0 ) )
27 6 26 syl 
 |-  ( A e. CC -> ( ( ( cos ` A ) ^ 2 ) =/= 0 <-> ( cos ` A ) =/= 0 ) )
28 27 biimpar 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( cos ` A ) ^ 2 ) =/= 0 )
29 11 25 12 28 divmul3d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) = -u 1 <-> ( ( sin ` A ) ^ 2 ) = ( -u 1 x. ( ( cos ` A ) ^ 2 ) ) ) )
30 29 necon3bid 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) =/= -u 1 <-> ( ( sin ` A ) ^ 2 ) =/= ( -u 1 x. ( ( cos ` A ) ^ 2 ) ) ) )
31 23 30 mpbird 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( sin ` A ) ^ 2 ) / ( ( cos ` A ) ^ 2 ) ) =/= -u 1 )
32 10 31 eqnetrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( tan ` A ) ^ 2 ) =/= -u 1 )
33 atandm3 
 |-  ( ( tan ` A ) e. dom arctan <-> ( ( tan ` A ) e. CC /\ ( ( tan ` A ) ^ 2 ) =/= -u 1 ) )
34 1 32 33 sylanbrc 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. dom arctan )