Theorem limsupubuz2

Description: A sequence with values in the extended reals, and with limsup that is not +oo , is eventually less than +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	limsupubuz2.1	⊢ Ⅎ 𝑗 𝜑
	limsupubuz2.2	⊢ Ⅎ 𝑗 𝐹
	limsupubuz2.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	limsupubuz2.4	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	limsupubuz2.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
	limsupubuz2.6	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
Assertion	limsupubuz2	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ )

Proof

Step	Hyp	Ref	Expression
1		limsupubuz2.1	⊢ Ⅎ 𝑗 𝜑
2		limsupubuz2.2	⊢ Ⅎ 𝑗 𝐹
3		limsupubuz2.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		limsupubuz2.4	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		limsupubuz2.5	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6		limsupubuz2.6	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) ≠ +∞ )
7	4	uzssre2	⊢ 𝑍 ⊆ ℝ
8	7	a1i	⊢ ( 𝜑 → 𝑍 ⊆ ℝ )
9	1 2 8 5 6	limsupub2	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) )
10	4	rexuzre	⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) ) )
11	3 10	syl	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ ↔ ∃ 𝑘 ∈ ℝ ∀ 𝑗 ∈ 𝑍 ( 𝑘 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) < +∞ ) ) )
12	9 11	mpbird	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ )