This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( 𝐹 ‘ 𝑗 ) < +∞ )