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 )