Metamath Proof Explorer

Theorem lmres

Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses lmres.2 
|- ( ph -> J e. ( TopOn ` X ) )
lmres.4 
|- ( ph -> F e. ( X ^pm CC ) )
lmres.5 
|- ( ph -> M e. ZZ )
Assertion lmres 
|- ( ph -> ( F ( ~~>t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~>t ` J ) P ) )

Proof

Step Hyp Ref Expression
1 lmres.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 lmres.4 
 |-  ( ph -> F e. ( X ^pm CC ) )
3 lmres.5 
 |-  ( ph -> M e. ZZ )
4 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 1 4 syl 
 |-  ( ph -> X e. J )
6 cnex 
 |-  CC e. _V
7 ssid 
 |-  X C_ X
8 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
9 zsscn 
 |-  ZZ C_ CC
10 8 9 sstri 
 |-  ( ZZ>= ` M ) C_ CC
11 pmss12g 
 |-  ( ( ( X C_ X /\ ( ZZ>= ` M ) C_ CC ) /\ ( X e. J /\ CC e. _V ) ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
12 7 10 11 mpanl12 
 |-  ( ( X e. J /\ CC e. _V ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
13 5 6 12 sylancl 
 |-  ( ph -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
14 fvex 
 |-  ( ZZ>= ` M ) e. _V
15 pmresg 
 |-  ( ( ( ZZ>= ` M ) e. _V /\ F e. ( X ^pm CC ) ) -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
16 14 2 15 sylancr 
 |-  ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
17 13 16 sseldd 
 |-  ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) )
18 17 2 2thd 
 |-  ( ph -> ( ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) <-> F e. ( X ^pm CC ) ) )
19 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
20 19 uztrn2 
 |-  ( ( j e. ( ZZ>= ` M ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` M ) )
21 dmres 
 |-  dom ( F |` ( ZZ>= ` M ) ) = ( ( ZZ>= ` M ) i^i dom F )
22 21 elin2 
 |-  ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> ( k e. ( ZZ>= ` M ) /\ k e. dom F ) )
23 22 baib 
 |-  ( k e. ( ZZ>= ` M ) -> ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> k e. dom F ) )
24 fvres 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
25 24 eleq1d 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u <-> ( F ` k ) e. u ) )
26 23 25 anbi12d 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
27 20 26 syl 
 |-  ( ( j e. ( ZZ>= ` M ) /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
28 27 ralbidva 
 |-  ( j e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
29 28 rexbiia 
 |-  ( E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) <-> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
30 29 imbi2i 
 |-  ( ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) ) <-> ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
31 30 ralbii 
 |-  ( A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) ) <-> A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
32 31 a1i 
 |-  ( ph -> ( A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) ) <-> A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
33 18 32 3anbi13d 
 |-  ( ph -> ( ( ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) ) ) <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
34 1 19 3 lmbr2 
 |-  ( ph -> ( ( F |` ( ZZ>= ` M ) ) ( ~~>t ` J ) P <-> ( ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) ) ) ) )
35 1 19 3 lmbr2 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. ( ZZ>= ` M ) A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
36 33 34 35 3bitr4rd 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~>t ` J ) P ) )