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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimlimsupleliminf.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimlimsupleliminf.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	xlimlimsupleliminf	⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xlimlimsupleliminf.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		xlimlimsupleliminf.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		xlimlimsupleliminf.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4	1 2 3	xlimliminflimsup	⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )
5	1 2 3	liminfgelimsupuz	⊢ ( 𝜑 → ( ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ↔ ( lim inf ‘ 𝐹 ) = ( lim sup ‘ 𝐹 ) ) )
6	4 5	bitr4d	⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( lim sup ‘ 𝐹 ) ≤ ( lim inf ‘ 𝐹 ) ) )