This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Glauco Siliprandi Limits limsupresuz2
Description: If the domain of a function is a subset of the integers, the superior
limit doesn't change when the function is restricted to an upper set of
integers. (Contributed by Glauco Siliprandi , 23-Oct-2021)
Ref
Expression
Hypotheses
limsupresuz2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
limsupresuz2.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
limsupresuz2.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
limsupresuz2.4 ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
Assertion
limsupresuz2 ⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim sup ‘ 𝐹 ) )
Proof
Step
Hyp
Ref
Expression
1
limsupresuz2.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2
limsupresuz2.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3
limsupresuz2.3 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4
limsupresuz2.4 ⊢ ( 𝜑 → dom 𝐹 ⊆ ℤ )
5
dmresss ⊢ dom ( 𝐹 ↾ ℝ ) ⊆ dom 𝐹
6
5
a1i ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ dom 𝐹 )
7
6 4
sstrd ⊢ ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
8
1 2 3 7
limsupresuz ⊢ ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ 𝑍 ) ) = ( lim sup ‘ 𝐹 ) )