Metamath Proof Explorer

Theorem supcnvlimsupmpt

Description: If a function on a set of upper integers has a real superior limit, the supremum of the rightmost parts of the function, converges to that superior limit. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supcnvlimsupmpt.j ⊢ Ⅎ j φ
supcnvlimsupmpt.m ⊢ φ → M ∈ ℤ
supcnvlimsupmpt.z ⊢ Z = ℤ ≥ M
supcnvlimsupmpt.b ⊢ φ ∧ j ∈ Z → B ∈ ℝ
supcnvlimsupmpt.r ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B ∈ ℝ
Assertion supcnvlimsupmpt ⊢ φ → k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < ⇝ lim sup ⁡ j ∈ Z ⟼ B

Proof

Step Hyp Ref Expression
1 supcnvlimsupmpt.j ⊢ Ⅎ j φ
2 supcnvlimsupmpt.m ⊢ φ → M ∈ ℤ
3 supcnvlimsupmpt.z ⊢ Z = ℤ ≥ M
4 supcnvlimsupmpt.b ⊢ φ ∧ j ∈ Z → B ∈ ℝ
5 supcnvlimsupmpt.r ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B ∈ ℝ
6 fveq2 ⊢ k = n → ℤ ≥ k = ℤ ≥ n
7 6 mpteq1d ⊢ k = n → j ∈ ℤ ≥ k ⟼ B = j ∈ ℤ ≥ n ⟼ B
8 7 rneqd ⊢ k = n → ran ⁡ j ∈ ℤ ≥ k ⟼ B = ran ⁡ j ∈ ℤ ≥ n ⟼ B
9 8 supeq1d ⊢ k = n → sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < = sup ran ⁡ j ∈ ℤ ≥ n ⟼ B ℝ * <
10 9 cbvmptv ⊢ k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < = n ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ n ⟼ B ℝ * <
11 3 uzssd3 ⊢ n ∈ Z → ℤ ≥ n ⊆ Z
12 11 adantl ⊢ φ ∧ n ∈ Z → ℤ ≥ n ⊆ Z
13 12 resmptd ⊢ φ ∧ n ∈ Z → j ∈ Z ⟼ B ↾ ℤ ≥ n = j ∈ ℤ ≥ n ⟼ B
14 13 eqcomd ⊢ φ ∧ n ∈ Z → j ∈ ℤ ≥ n ⟼ B = j ∈ Z ⟼ B ↾ ℤ ≥ n
15 14 rneqd ⊢ φ ∧ n ∈ Z → ran ⁡ j ∈ ℤ ≥ n ⟼ B = ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ n
16 15 supeq1d ⊢ φ ∧ n ∈ Z → sup ran ⁡ j ∈ ℤ ≥ n ⟼ B ℝ * < = sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ n ℝ * <
17 16 mpteq2dva ⊢ φ → n ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ n ⟼ B ℝ * < = n ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ n ℝ * <
18 10 17 syl5eq ⊢ φ → k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < = n ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ n ℝ * <
19 1 4 fmptd2f ⊢ φ → j ∈ Z ⟼ B : Z ⟶ ℝ
20 2 3 19 5 supcnvlimsup ⊢ φ → n ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ n ℝ * < ⇝ lim sup ⁡ j ∈ Z ⟼ B
21 18 20 eqbrtrd ⊢ φ → k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < ⇝ lim sup ⁡ j ∈ Z ⟼ B