Metamath Proof Explorer

Theorem bndatandm

Description: A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion bndatandm 
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. dom arctan )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. CC )
2 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
3 2 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 2 ) e. CC )
4 3 abscld 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A ^ 2 ) ) e. RR )
5 2nn0 
 |-  2 e. NN0
6 absexp 
 |-  ( ( A e. CC /\ 2 e. NN0 ) -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) )
7 1 5 6 sylancl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A ^ 2 ) ) = ( ( abs ` A ) ^ 2 ) )
8 simpr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) < 1 )
9 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
10 9 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` A ) e. RR )
11 1red 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 1 e. RR )
12 absge0 
 |-  ( A e. CC -> 0 <_ ( abs ` A ) )
13 12 adantr 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 <_ ( abs ` A ) )
14 0le1 
 |-  0 <_ 1
15 14 a1i 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> 0 <_ 1 )
16 10 11 13 15 lt2sqd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) < 1 <-> ( ( abs ` A ) ^ 2 ) < ( 1 ^ 2 ) ) )
17 8 16 mpbid 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) ^ 2 ) < ( 1 ^ 2 ) )
18 sq1 
 |-  ( 1 ^ 2 ) = 1
19 17 18 breqtrdi 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( ( abs ` A ) ^ 2 ) < 1 )
20 7 19 eqbrtrd 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A ^ 2 ) ) < 1 )
21 4 20 ltned 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( abs ` ( A ^ 2 ) ) =/= 1 )
22 fveq2 
 |-  ( ( A ^ 2 ) = -u 1 -> ( abs ` ( A ^ 2 ) ) = ( abs ` -u 1 ) )
23 ax-1cn 
 |-  1 e. CC
24 23 absnegi 
 |-  ( abs ` -u 1 ) = ( abs ` 1 )
25 abs1 
 |-  ( abs ` 1 ) = 1
26 24 25 eqtri 
 |-  ( abs ` -u 1 ) = 1
27 22 26 eqtrdi 
 |-  ( ( A ^ 2 ) = -u 1 -> ( abs ` ( A ^ 2 ) ) = 1 )
28 27 necon3i 
 |-  ( ( abs ` ( A ^ 2 ) ) =/= 1 -> ( A ^ 2 ) =/= -u 1 )
29 21 28 syl 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> ( A ^ 2 ) =/= -u 1 )
30 atandm3 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
31 1 29 30 sylanbrc 
 |-  ( ( A e. CC /\ ( abs ` A ) < 1 ) -> A e. dom arctan )