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	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimmnflimsup2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimmnflimsup2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	xlimmnflimsup2	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimmnflimsup2.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		xlimmnflimsup2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		xlimmnflimsup2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4	1 2 3	xlimmnfv	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}jF$$
6	5 1 2 3	limsupmnfuz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists k\in Z\forall j\in {\mathbb{Z}}_{\ge k}F\left(j\right)\le x\right)$$
7	4 6	bitr4d	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \mathrm{lim\; sup}\left(F\right)=\mathrm{-\infty }\right)$$