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

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 ⊢ Ⅎ 𝑗 𝜑
limsupvaluzmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupvaluzmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupvaluzmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
Assertion limsupvaluzmpt ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 limsupvaluzmpt.j ⊢ Ⅎ 𝑗 𝜑
2 limsupvaluzmpt.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 limsupvaluzmpt.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 limsupvaluzmpt.b ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → 𝐵 ∈ ℝ* )
5 1 4 fmptd2f ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) : 𝑍 ⟶ ℝ* )
6 2 3 5 limsupvaluz ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) )
7 3 uzssd3 ⊢ ( 𝑘 ∈ 𝑍 → ( ℤ≥ ‘ 𝑘 ) ⊆ 𝑍 )
8 7 resmptd ⊢ ( 𝑘 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) )
9 8 rneqd ⊢ ( 𝑘 ∈ 𝑍 → ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) = ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) )
10 9 supeq1d ⊢ ( 𝑘 ∈ 𝑍 → sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) = sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) )
11 10 mpteq2ia ⊢ ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) )
12 11 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) )
13 12 rneqd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) = ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) )
14 13 infeq1d ⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ↾ ( ℤ≥ ‘ 𝑘 ) ) , ℝ* , < ) ) , ℝ* , < ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) , ℝ* , < ) )
15 6 14 eqtrd ⊢ ( 𝜑 → ( lim sup ‘ ( 𝑗 ∈ 𝑍 ↦ 𝐵 ) ) = inf ( ran ( 𝑘 ∈ 𝑍 ↦ sup ( ran ( 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ↦ 𝐵 ) , ℝ* , < ) ) , ℝ* , < ) )