Description: Closure of the limit of a sequence of complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014) (Revised by Mario Carneiro, 28-Apr-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rlimcl | |- ( F ~~>r A -> A e. CC ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rlimf | |- ( F ~~>r A -> F : dom F --> CC ) |
|
| 2 | rlimss | |- ( F ~~>r A -> dom F C_ RR ) |
|
| 3 | eqidd | |- ( ( F ~~>r A /\ x e. dom F ) -> ( F ` x ) = ( F ` x ) ) |
|
| 4 | 1 2 3 | rlim | |- ( F ~~>r A -> ( F ~~>r A <-> ( A e. CC /\ A. y e. RR+ E. z e. RR A. x e. dom F ( z <_ x -> ( abs ` ( ( F ` x ) - A ) ) < y ) ) ) ) |
| 5 | 4 | ibi | |- ( F ~~>r A -> ( A e. CC /\ A. y e. RR+ E. z e. RR A. x e. dom F ( z <_ x -> ( abs ` ( ( F ` x ) - A ) ) < y ) ) ) |
| 6 | 5 | simpld | |- ( F ~~>r A -> A e. CC ) |