Theorem atans

Description: The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	atansopn.d	|- D = ( CC \ ( -oo (,] 0 ) )
	atansopn.s	|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
Assertion	atans	|- ( A e. S <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. D ) )

Proof

Step	Hyp	Ref	Expression
1		atansopn.d	|- D = ( CC \ ( -oo (,] 0 ) )
2		atansopn.s	|- S = { y e. CC | ( 1 + ( y ^ 2 ) ) e. D }
3		oveq1	|- ( y = A -> ( y ^ 2 ) = ( A ^ 2 ) )
4	3	oveq2d	|- ( y = A -> ( 1 + ( y ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) )
5	4	eleq1d	|- ( y = A -> ( ( 1 + ( y ^ 2 ) ) e. D <-> ( 1 + ( A ^ 2 ) ) e. D ) )
6	5 2	elrab2	|- ( A e. S <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) e. D ) )