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
|- ( ph -> M e. ZZ )
limsupresuz.z
|- Z = ( ZZ>= ` M )
limsupresuz.f
|- ( ph -> F e. V )
limsupresuz.d
|- ( ph -> dom ( F |` RR ) C_ ZZ )
Assertion limsupresuz
|- ( ph -> ( limsup ` ( F |` Z ) ) = ( limsup ` F ) )

Proof

Step Hyp Ref Expression
1 limsupresuz.m
 |-  ( ph -> M e. ZZ )
2 limsupresuz.z
 |-  Z = ( ZZ>= ` M )
3 limsupresuz.f
 |-  ( ph -> F e. V )
4 limsupresuz.d
 |-  ( ph -> dom ( F |` RR ) C_ ZZ )
5 rescom
 |-  ( ( F |` Z ) |` RR ) = ( ( F |` RR ) |` Z )
6 5 fveq2i
 |-  ( limsup ` ( ( F |` Z ) |` RR ) ) = ( limsup ` ( ( F |` RR ) |` Z ) )
7 6 a1i
 |-  ( ph -> ( limsup ` ( ( F |` Z ) |` RR ) ) = ( limsup ` ( ( F |` RR ) |` Z ) ) )
8 relres
 |-  Rel ( F |` RR )
9 8 a1i
 |-  ( ph -> Rel ( F |` RR ) )
10 relssres
 |-  ( ( Rel ( F |` RR ) /\ dom ( F |` RR ) C_ ZZ ) -> ( ( F |` RR ) |` ZZ ) = ( F |` RR ) )
11 9 4 10 syl2anc
 |-  ( ph -> ( ( F |` RR ) |` ZZ ) = ( F |` RR ) )
12 11 eqcomd
 |-  ( ph -> ( F |` RR ) = ( ( F |` RR ) |` ZZ ) )
13 12 reseq1d
 |-  ( ph -> ( ( F |` RR ) |` ( M [,) +oo ) ) = ( ( ( F |` RR ) |` ZZ ) |` ( M [,) +oo ) ) )
14 resres
 |-  ( ( ( F |` RR ) |` ZZ ) |` ( M [,) +oo ) ) = ( ( F |` RR ) |` ( ZZ i^i ( M [,) +oo ) ) )
15 14 a1i
 |-  ( ph -> ( ( ( F |` RR ) |` ZZ ) |` ( M [,) +oo ) ) = ( ( F |` RR ) |` ( ZZ i^i ( M [,) +oo ) ) ) )
16 1 2 uzinico
 |-  ( ph -> Z = ( ZZ i^i ( M [,) +oo ) ) )
17 16 eqcomd
 |-  ( ph -> ( ZZ i^i ( M [,) +oo ) ) = Z )
18 17 reseq2d
 |-  ( ph -> ( ( F |` RR ) |` ( ZZ i^i ( M [,) +oo ) ) ) = ( ( F |` RR ) |` Z ) )
19 13 15 18 3eqtrrd
 |-  ( ph -> ( ( F |` RR ) |` Z ) = ( ( F |` RR ) |` ( M [,) +oo ) ) )
20 19 fveq2d
 |-  ( ph -> ( limsup ` ( ( F |` RR ) |` Z ) ) = ( limsup ` ( ( F |` RR ) |` ( M [,) +oo ) ) ) )
21 1 zred
 |-  ( ph -> M e. RR )
22 eqid
 |-  ( M [,) +oo ) = ( M [,) +oo )
23 3 resexd
 |-  ( ph -> ( F |` RR ) e. _V )
24 21 22 23 limsupresico
 |-  ( ph -> ( limsup ` ( ( F |` RR ) |` ( M [,) +oo ) ) ) = ( limsup ` ( F |` RR ) ) )
25 20 24 eqtrd
 |-  ( ph -> ( limsup ` ( ( F |` RR ) |` Z ) ) = ( limsup ` ( F |` RR ) ) )
26 7 25 eqtrd
 |-  ( ph -> ( limsup ` ( ( F |` Z ) |` RR ) ) = ( limsup ` ( F |` RR ) ) )
27 3 resexd
 |-  ( ph -> ( F |` Z ) e. _V )
28 27 limsupresre
 |-  ( ph -> ( limsup ` ( ( F |` Z ) |` RR ) ) = ( limsup ` ( F |` Z ) ) )
29 3 limsupresre
 |-  ( ph -> ( limsup ` ( F |` RR ) ) = ( limsup ` F ) )
30 26 28 29 3eqtr3d
 |-  ( ph -> ( limsup ` ( F |` Z ) ) = ( limsup ` F ) )