Theorem xlimpnfliminf

Description: If a sequence of extended reals converges to +oo then its superior limit is also +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimpnfliminf.m	|- ( ph -> M e. ZZ )
	xlimpnfliminf.z	|- Z = ( ZZ>= ` M )
	xlimpnfliminf.f	|- ( ph -> F : Z --> RR* )
	xlimpnfliminf.c	|- ( ph -> F ~~>* +oo )
Assertion	xlimpnfliminf	|- ( ph -> ( liminf ` F ) = +oo )

Proof

Step	Hyp	Ref	Expression
1		xlimpnfliminf.m	|- ( ph -> M e. ZZ )
2		xlimpnfliminf.z	|- Z = ( ZZ>= ` M )
3		xlimpnfliminf.f	|- ( ph -> F : Z --> RR* )
4		xlimpnfliminf.c	|- ( ph -> F ~~>* +oo )
5	1 2 3	xlimpnfv	|- ( ph -> ( F ~~>* +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
6	4 5	mpbid	|- ( ph -> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
7		nfcv	|- F/_ j F
8	7 1 2 3	liminfpnfuz	|- ( ph -> ( ( liminf ` F ) = +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
9	6 8	mpbird	|- ( ph -> ( liminf ` F ) = +oo )