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 ) )