Theorem xlimmnflimsup2

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

Proof

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