Metamath Proof Explorer

Theorem liminfresuz

Description: If the real part of the domain of a function is a subset of the integers, the inferior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses liminfresuz.m 
|- ( ph -> M e. ZZ )
liminfresuz.z 
|- Z = ( ZZ>= ` M )
liminfresuz.f 
|- ( ph -> F e. V )
liminfresuz.d 
|- ( ph -> dom ( F |` RR ) C_ ZZ )
Assertion liminfresuz 
|- ( ph -> ( liminf ` ( F |` Z ) ) = ( liminf ` F ) )

Proof

Step Hyp Ref Expression
1 liminfresuz.m 
 |-  ( ph -> M e. ZZ )
2 liminfresuz.z 
 |-  Z = ( ZZ>= ` M )
3 liminfresuz.f 
 |-  ( ph -> F e. V )
4 liminfresuz.d 
 |-  ( ph -> dom ( F |` RR ) C_ ZZ )
5 rescom 
 |-  ( ( F |` Z ) |` RR ) = ( ( F |` RR ) |` Z )
6 5 fveq2i 
 |-  ( liminf ` ( ( F |` Z ) |` RR ) ) = ( liminf ` ( ( F |` RR ) |` Z ) )
7 6 a1i 
 |-  ( ph -> ( liminf ` ( ( F |` Z ) |` RR ) ) = ( liminf ` ( ( 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 -> ( liminf ` ( ( F |` RR ) |` Z ) ) = ( liminf ` ( ( 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 liminfresico 
 |-  ( ph -> ( liminf ` ( ( F |` RR ) |` ( M [,) +oo ) ) ) = ( liminf ` ( F |` RR ) ) )
25 20 24 eqtrd 
 |-  ( ph -> ( liminf ` ( ( F |` RR ) |` Z ) ) = ( liminf ` ( F |` RR ) ) )
26 7 25 eqtrd 
 |-  ( ph -> ( liminf ` ( ( F |` Z ) |` RR ) ) = ( liminf ` ( F |` RR ) ) )
27 3 resexd 
 |-  ( ph -> ( F |` Z ) e. _V )
28 27 liminfresre 
 |-  ( ph -> ( liminf ` ( ( F |` Z ) |` RR ) ) = ( liminf ` ( F |` Z ) ) )
29 3 liminfresre 
 |-  ( ph -> ( liminf ` ( F |` RR ) ) = ( liminf ` F ) )
30 26 28 29 3eqtr3d 
 |-  ( ph -> ( liminf ` ( F |` Z ) ) = ( liminf ` F ) )