Description: A sequence of extended reals converges to +oo if and only if its superior limit is also +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | xlimpnfliminf2.m | |- ( ph -> M e. ZZ ) |
|
| xlimpnfliminf2.z | |- Z = ( ZZ>= ` M ) |
||
| xlimpnfliminf2.f | |- ( ph -> F : Z --> RR* ) |
||
| Assertion | xlimpnfliminf2 | |- ( ph -> ( F ~~>* +oo <-> ( liminf ` F ) = +oo ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xlimpnfliminf2.m | |- ( ph -> M e. ZZ ) |
|
| 2 | xlimpnfliminf2.z | |- Z = ( ZZ>= ` M ) |
|
| 3 | xlimpnfliminf2.f | |- ( ph -> F : Z --> RR* ) |
|
| 4 | 1 2 3 | xlimpnfv | |- ( ph -> ( F ~~>* +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) ) |
| 5 | nfcv | |- F/_ j F |
|
| 6 | 5 1 2 3 | liminfpnfuz | |- ( ph -> ( ( liminf ` F ) = +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) ) |
| 7 | 4 6 | bitr4d | |- ( ph -> ( F ~~>* +oo <-> ( liminf ` F ) = +oo ) ) |