Description: A real valued sequence that converges w.r.t. the topology on the complex numbers, converges w.r.t. the topology on the extended reals (Contributed by Glauco Siliprandi, 23-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | dmclimxlim.1 | |- ( ph -> M e. ZZ ) |
|
| dmclimxlim.2 | |- Z = ( ZZ>= ` M ) |
||
| dmclimxlim.3 | |- ( ph -> F : Z --> RR ) |
||
| dmclimxlim.4 | |- ( ph -> F e. dom ~~> ) |
||
| Assertion | dmclimxlim | |- ( ph -> F e. dom ~~>* ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmclimxlim.1 | |- ( ph -> M e. ZZ ) |
|
| 2 | dmclimxlim.2 | |- Z = ( ZZ>= ` M ) |
|
| 3 | dmclimxlim.3 | |- ( ph -> F : Z --> RR ) |
|
| 4 | dmclimxlim.4 | |- ( ph -> F e. dom ~~> ) |
|
| 5 | xlimrel | |- Rel ~~>* |
|
| 6 | 1 2 3 | climliminf | |- ( ph -> ( F e. dom ~~> <-> F ~~> ( liminf ` F ) ) ) |
| 7 | 4 6 | mpbid | |- ( ph -> F ~~> ( liminf ` F ) ) |
| 8 | 1 2 3 7 | climxlim | |- ( ph -> F ~~>* ( liminf ` F ) ) |
| 9 | releldm | |- ( ( Rel ~~>* /\ F ~~>* ( liminf ` F ) ) -> F e. dom ~~>* ) |
|
| 10 | 5 8 9 | sylancr | |- ( ph -> F e. dom ~~>* ) |