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 )