Metamath Proof Explorer

Theorem limsupvaluzmpt

Description: The superior limit, when the domain of the function is a set of upper integers (the first condition is needed, otherwise the l.h.s. would be -oo and the r.h.s. would be +oo ). (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsupvaluzmpt.j ⊢ Ⅎ j φ
2 limsupvaluzmpt.m ⊢ φ → M ∈ ℤ
3 limsupvaluzmpt.z ⊢ Z = ℤ ≥ M
4 limsupvaluzmpt.b ⊢ φ ∧ j ∈ Z → B ∈ ℝ *
5 1 4 fmptd2f ⊢ φ → j ∈ Z ⟼ B : Z ⟶ ℝ *
6 2 3 5 limsupvaluz ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B = inf ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < ℝ * <
7 3 uzssd3 ⊢ k ∈ Z → ℤ ≥ k ⊆ Z
8 7 resmptd ⊢ k ∈ Z → j ∈ Z ⟼ B ↾ ℤ ≥ k = j ∈ ℤ ≥ k ⟼ B
9 8 rneqd ⊢ k ∈ Z → ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k = ran ⁡ j ∈ ℤ ≥ k ⟼ B
10 9 supeq1d ⊢ k ∈ Z → sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < = sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * <
11 10 mpteq2ia ⊢ k ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < = k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * <
12 11 a1i ⊢ φ → k ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < = k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * <
13 12 rneqd ⊢ φ → ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < = ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * <
14 13 infeq1d ⊢ φ → inf ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ Z ⟼ B ↾ ℤ ≥ k ℝ * < ℝ * < = inf ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < ℝ * <
15 6 14 eqtrd ⊢ φ → lim sup ⁡ j ∈ Z ⟼ B = inf ran ⁡ k ∈ Z ⟼ sup ran ⁡ j ∈ ℤ ≥ k ⟼ B ℝ * < ℝ * <