Theorem xlimmnflimsup2

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

Proof

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