Metamath Proof Explorer


Theorem limsupresuz

Description: If the real part of 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 limsupresuz.m ( 𝜑𝑀 ∈ ℤ )
limsupresuz.z 𝑍 = ( ℤ𝑀 )
limsupresuz.f ( 𝜑𝐹𝑉 )
limsupresuz.d ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
Assertion limsupresuz ( 𝜑 → ( lim sup ‘ ( 𝐹𝑍 ) ) = ( lim sup ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 limsupresuz.m ( 𝜑𝑀 ∈ ℤ )
2 limsupresuz.z 𝑍 = ( ℤ𝑀 )
3 limsupresuz.f ( 𝜑𝐹𝑉 )
4 limsupresuz.d ( 𝜑 → dom ( 𝐹 ↾ ℝ ) ⊆ ℤ )
5 rescom ( ( 𝐹𝑍 ) ↾ ℝ ) = ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 )
6 5 fveq2i ( lim sup ‘ ( ( 𝐹𝑍 ) ↾ ℝ ) ) = ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) )
7 6 a1i ( 𝜑 → ( lim sup ‘ ( ( 𝐹𝑍 ) ↾ ℝ ) ) = ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) )
8 relres Rel ( 𝐹 ↾ ℝ )
9 8 a1i ( 𝜑 → Rel ( 𝐹 ↾ ℝ ) )
10 relssres ( ( Rel ( 𝐹 ↾ ℝ ) ∧ dom ( 𝐹 ↾ ℝ ) ⊆ ℤ ) → ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) = ( 𝐹 ↾ ℝ ) )
11 9 4 10 syl2anc ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) = ( 𝐹 ↾ ℝ ) )
12 11 eqcomd ( 𝜑 → ( 𝐹 ↾ ℝ ) = ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) )
13 12 reseq1d ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) )
14 resres ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )
15 14 a1i ( 𝜑 → ( ( ( 𝐹 ↾ ℝ ) ↾ ℤ ) ↾ ( 𝑀 [,) +∞ ) ) = ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) )
16 1 2 uzinico ( 𝜑𝑍 = ( ℤ ∩ ( 𝑀 [,) +∞ ) ) )
17 16 eqcomd ( 𝜑 → ( ℤ ∩ ( 𝑀 [,) +∞ ) ) = 𝑍 )
18 17 reseq2d ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ ( ℤ ∩ ( 𝑀 [,) +∞ ) ) ) = ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) )
19 13 15 18 3eqtrrd ( 𝜑 → ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) = ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) )
20 19 fveq2d ( 𝜑 → ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) = ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) ) )
21 1 zred ( 𝜑𝑀 ∈ ℝ )
22 eqid ( 𝑀 [,) +∞ ) = ( 𝑀 [,) +∞ )
23 3 resexd ( 𝜑 → ( 𝐹 ↾ ℝ ) ∈ V )
24 21 22 23 limsupresico ( 𝜑 → ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ ( 𝑀 [,) +∞ ) ) ) = ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) )
25 20 24 eqtrd ( 𝜑 → ( lim sup ‘ ( ( 𝐹 ↾ ℝ ) ↾ 𝑍 ) ) = ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) )
26 7 25 eqtrd ( 𝜑 → ( lim sup ‘ ( ( 𝐹𝑍 ) ↾ ℝ ) ) = ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) )
27 3 resexd ( 𝜑 → ( 𝐹𝑍 ) ∈ V )
28 27 limsupresre ( 𝜑 → ( lim sup ‘ ( ( 𝐹𝑍 ) ↾ ℝ ) ) = ( lim sup ‘ ( 𝐹𝑍 ) ) )
29 3 limsupresre ( 𝜑 → ( lim sup ‘ ( 𝐹 ↾ ℝ ) ) = ( lim sup ‘ 𝐹 ) )
30 26 28 29 3eqtr3d ( 𝜑 → ( lim sup ‘ ( 𝐹𝑍 ) ) = ( lim sup ‘ 𝐹 ) )