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=supran⁡k∈Z⟼supran⁡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=supran⁡k∈Z⟼supran⁡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→supran⁡j∈Z⟼B↾ℤ≥kℝ*<=supran⁡j∈ℤ≥k⟼Bℝ*<
11 10 mpteq2ia ⊢k∈Z⟼supran⁡j∈Z⟼B↾ℤ≥kℝ*<=k∈Z⟼supran⁡j∈ℤ≥k⟼Bℝ*<
12 11 a1i ⊢φ→k∈Z⟼supran⁡j∈Z⟼B↾ℤ≥kℝ*<=k∈Z⟼supran⁡j∈ℤ≥k⟼Bℝ*<
13 12 rneqd ⊢φ→ran⁡k∈Z⟼supran⁡j∈Z⟼B↾ℤ≥kℝ*<=ran⁡k∈Z⟼supran⁡j∈ℤ≥k⟼Bℝ*<
14 13 infeq1d ⊢φ→supran⁡k∈Z⟼supran⁡j∈Z⟼B↾ℤ≥kℝ*<ℝ*<=supran⁡k∈Z⟼supran⁡j∈ℤ≥k⟼Bℝ*<ℝ*<
15 6 14 eqtrd ⊢φ→lim sup⁡j∈Z⟼B=supran⁡k∈Z⟼supran⁡j∈ℤ≥k⟼Bℝ*<ℝ*<