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 ⊢ Ⅎ j φ
limsupubuz2.2 ⊢ Ⅎ _ j F
limsupubuz2.3 ⊢ φ → M ∈ ℤ
limsupubuz2.4 ⊢ Z = ℤ ≥ M
limsupubuz2.5 ⊢ φ → F : Z ⟶ ℝ *
limsupubuz2.6 ⊢ φ → lim sup ⁡ F ≠ +∞
Assertion limsupubuz2 ⊢ φ → ∃ k ∈ Z ∀ j ∈ ℤ ≥ k F ⁡ j < +∞

Proof

Step Hyp Ref Expression
1 limsupubuz2.1 ⊢ Ⅎ j φ
2 limsupubuz2.2 ⊢ Ⅎ _ j F
3 limsupubuz2.3 ⊢ φ → M ∈ ℤ
4 limsupubuz2.4 ⊢ Z = ℤ ≥ M
5 limsupubuz2.5 ⊢ φ → F : Z ⟶ ℝ *
6 limsupubuz2.6 ⊢ φ → lim sup ⁡ F ≠ +∞
7 4 uzssre2 ⊢ Z ⊆ ℝ
8 7 a1i ⊢ φ → Z ⊆ ℝ
9 1 2 8 5 6 limsupub2 ⊢ φ → ∃ k ∈ ℝ ∀ j ∈ Z k ≤ j → F ⁡ j < +∞
10 4 rexuzre ⊢ M ∈ ℤ → ∃ k ∈ Z ∀ j ∈ ℤ ≥ k F ⁡ j < +∞ ↔ ∃ k ∈ ℝ ∀ j ∈ Z k ≤ j → F ⁡ j < +∞
11 3 10 syl ⊢ φ → ∃ k ∈ Z ∀ j ∈ ℤ ≥ k F ⁡ j < +∞ ↔ ∃ k ∈ ℝ ∀ j ∈ Z k ≤ j → F ⁡ j < +∞
12 9 11 mpbird ⊢ φ → ∃ k ∈ Z ∀ j ∈ ℤ ≥ k F ⁡ j < +∞