Theorem xlimpnfliminf

Description: If a sequence of extended reals converges to +oo then its superior limit is also +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimpnfliminf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	xlimpnfliminf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	xlimpnfliminf.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
	xlimpnfliminf.c	⊢ ( 𝜑 → 𝐹 ~~>* +∞ )
Assertion	xlimpnfliminf	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = +∞ )

Proof

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