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