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

Metamath Proof Explorer

Theorem limsupubuzmpt

Description: If the limsup is not +oo , then the function is eventually bounded. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupubuzmpt.j ⊢ Ⅎ j φ
limsupubuzmpt.z ⊢ Z = ℤ ≥ M
limsupubuzmpt.b ⊢ φ ∧ j ∈ Z → B ∈ ℝ
limsupubuzmpt.n ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B ≠ +∞
Assertion limsupubuzmpt ⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z B ≤ x

Proof

Step Hyp Ref Expression
1 limsupubuzmpt.j ⊢ Ⅎ j φ
2 limsupubuzmpt.z ⊢ Z = ℤ ≥ M
3 limsupubuzmpt.b ⊢ φ ∧ j ∈ Z → B ∈ ℝ
4 limsupubuzmpt.n ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B ≠ +∞
5 nfmpt1 ⊢ Ⅎ _ j j ∈ Z ⟼ B
6 eqid ⊢ j ∈ Z ⟼ B = j ∈ Z ⟼ B
7 1 3 6 fmptdf ⊢ φ → j ∈ Z ⟼ B : Z ⟶ ℝ
8 5 2 7 4 limsupubuz ⊢ φ → ∃ y ∈ ℝ ∀ j ∈ Z j ∈ Z ⟼ B ⁡ j ≤ y
9 6 a1i ⊢ φ → j ∈ Z ⟼ B = j ∈ Z ⟼ B
10 9 3 fvmpt2d ⊢ φ ∧ j ∈ Z → j ∈ Z ⟼ B ⁡ j = B
11 10 breq1d ⊢ φ ∧ j ∈ Z → j ∈ Z ⟼ B ⁡ j ≤ y ↔ B ≤ y
12 1 11 ralbida ⊢ φ → ∀ j ∈ Z j ∈ Z ⟼ B ⁡ j ≤ y ↔ ∀ j ∈ Z B ≤ y
13 12 rexbidv ⊢ φ → ∃ y ∈ ℝ ∀ j ∈ Z j ∈ Z ⟼ B ⁡ j ≤ y ↔ ∃ y ∈ ℝ ∀ j ∈ Z B ≤ y
14 8 13 mpbid ⊢ φ → ∃ y ∈ ℝ ∀ j ∈ Z B ≤ y
15 breq2 ⊢ y = x → B ≤ y ↔ B ≤ x
16 15 ralbidv ⊢ y = x → ∀ j ∈ Z B ≤ y ↔ ∀ j ∈ Z B ≤ x
17 16 cbvrexvw ⊢ ∃ y ∈ ℝ ∀ j ∈ Z B ≤ y ↔ ∃ x ∈ ℝ ∀ j ∈ Z B ≤ x
18 14 17 sylib ⊢ φ → ∃ x ∈ ℝ ∀ j ∈ Z B ≤ x