Theorem xlimmnflimsup

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	xlimmnflimsup.m	|- ( ph -> M e. ZZ )
	xlimmnflimsup.z	|- Z = ( ZZ>= ` M )
	xlimmnflimsup.f	|- ( ph -> F : Z --> RR* )
	xlimmnflimsup.c	|- ( ph -> F ~~>* -oo )
Assertion	xlimmnflimsup	|- ( ph -> ( limsup ` F ) = -oo )

Proof

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