Metamath Proof Explorer


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 ) )