Theorem xlimpnfliminf2

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	xlimpnfliminf2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimpnfliminf2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimpnfliminf2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	xlimpnfliminf2	⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( lim inf ‘ 𝐹 ) = +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		xlimpnfliminf2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		xlimpnfliminf2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		xlimpnfliminf2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4	1 2 3	xlimpnfv	⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
5		nfcv	⊢ Ⅎ 𝑗 𝐹
6	5 1 2 3	liminfpnfuz	⊢ ( 𝜑 → ( ( lim inf ‘ 𝐹 ) = +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
7	4 6	bitr4d	⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( lim inf ‘ 𝐹 ) = +∞ ) )