Theorem xlimmnflimsup

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

Proof

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