This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atanre

Description: A real number is in the domain of the arctangent function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atanre 
|- ( A e. RR -> A e. dom arctan )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 neg1rr 
 |-  -u 1 e. RR
3 2 a1i 
 |-  ( A e. RR -> -u 1 e. RR )
4 0red 
 |-  ( A e. RR -> 0 e. RR )
5 resqcl 
 |-  ( A e. RR -> ( A ^ 2 ) e. RR )
6 neg1lt0 
 |-  -u 1 < 0
7 6 a1i 
 |-  ( A e. RR -> -u 1 < 0 )
8 sqge0 
 |-  ( A e. RR -> 0 <_ ( A ^ 2 ) )
9 3 4 5 7 8 ltletrd 
 |-  ( A e. RR -> -u 1 < ( A ^ 2 ) )
10 3 9 gtned 
 |-  ( A e. RR -> ( A ^ 2 ) =/= -u 1 )
11 atandm3 
 |-  ( A e. dom arctan <-> ( A e. CC /\ ( A ^ 2 ) =/= -u 1 ) )
12 1 10 11 sylanbrc 
 |-  ( A e. RR -> A e. dom arctan )