Theorem xlimlimsupleliminf

Description: A sequence of extended reals converges if and only if its superior limit is smaller than or equal to its inferior limit. (Contributed by Glauco Siliprandi, 2-Dec-2023)

	Ref	Expression
Hypotheses	xlimlimsupleliminf.1	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimlimsupleliminf.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimlimsupleliminf.3	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
Assertion	xlimlimsupleliminf	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow \mathrm{lim\; sup}\left(F\right)\le \mathrm{lim\; inf}\left(F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimlimsupleliminf.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		xlimlimsupleliminf.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		xlimlimsupleliminf.3	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4	1 2 3	xlimliminflimsup	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow \mathrm{lim\; inf}\left(F\right)=\mathrm{lim\; sup}\left(F\right)\right)$$
5	1 2 3	liminfgelimsupuz	$$⊢\phi \to \left(\mathrm{lim\; sup}\left(F\right)\le \mathrm{lim\; inf}\left(F\right)\leftrightarrow \mathrm{lim\; inf}\left(F\right)=\mathrm{lim\; sup}\left(F\right)\right)$$
6	4 5	bitr4d	$$⊢\phi \to \left(F\in \mathrm{dom}\underset{*}{⇝}\leftrightarrow \mathrm{lim\; sup}\left(F\right)\le \mathrm{lim\; inf}\left(F\right)\right)$$