MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmres Structured version   Unicode version
Theorem lmres 20092
Description: A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
Hypotheses
Ref Expression
lmres.2 |- ( ph -> J e. (TopOn ` X ) )
lmres.4 |- ( ph -> F e. ( X ^pm CC ) )
lmres.5 |- ( ph -> M e. ZZ )
Assertion
Ref Expression
lmres |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~> t ` J ) P ) )
Proof of Theorem lmres
Dummy variables j k u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lmres.2 . . . . . . 7 |- ( ph -> J e. (TopOn ` X ) )
2 toponmax 19719 . . . . . . 7 |- ( J e. (TopOn ` X ) -> X e. J )
31, 2syl 17 . . . . . 6 |- ( ph -> X e. J )
4 cnex 9602 . . . . . 6 |- CC e. _V
5 ssid 3460 . . . . . . 7 |- X C_ X
6 uzssz 11145 . . . . . . . 8 |- ( ZZ>= ` M ) C_ ZZ
7 zsscn 10912 . . . . . . . 8 |- ZZ C_ CC
86, 7sstri 3450 . . . . . . 7 |- ( ZZ>= ` M ) C_ CC
9 pmss12g 7482 . . . . . . 7 |- ( ( ( X C_ X /\ ( ZZ>= ` M ) C_ CC ) /\ ( X e. J /\ CC e. _V ) ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
105, 8, 9mpanl12 680 . . . . . 6 |- ( ( X e. J /\ CC e. _V ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
113, 4, 10sylancl 660 . . . . 5 |- ( ph -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
12 fvex 5858 . . . . . 6 |- ( ZZ>= ` M ) e. _V
13 lmres.4 . . . . . 6 |- ( ph -> F e. ( X ^pm CC ) )
14 pmresg 7483 . . . . . 6 |- ( ( ( ZZ>= ` M ) e. _V /\ F e. ( X ^pm CC ) ) -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
1512, 13, 14sylancr 661 . . . . 5 |- ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
1611, 15sseldd 3442 . . . 4 |- ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) )
1716, 132thd 240 . . 3 |- ( ph -> ( ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) <-> F e. ( X ^pm CC ) ) )
18 eqid 2402 . . . . . . . . . 10 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
1918uztrn2 11143 . . . . . . . . 9 |- ( ( j e. ( ZZ>= ` M ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` M ) )
20 dmres 5113 . . . . . . . . . . . 12 |- dom ( F |` ( ZZ>= ` M ) ) = ( ( ZZ>= ` M ) i^i dom F )
2120elin2 3629 . . . . . . . . . . 11 |- ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> ( k e. ( ZZ>= ` M ) /\ k e. dom F ) )
2221baib 904 . . . . . . . . . 10 |- ( k e. ( ZZ>= ` M ) -> ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> k e. dom F ) )
23 fvres 5862 . . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
2423eleq1d 2471 . . . . . . . . . 10 |- ( k e. ( ZZ>= ` M ) -> ( ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u <-> ( F ` k ) e. u ) )
2522, 24anbi12d 709 . . . . . . . . 9 |- ( k e. ( ZZ>= ` M ) -> ( ( k e. dom ( F |` ( ZZ>= ` M ) ) /\ ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. u ) ) )
2619, 25syl 17 . . . . . . . 8 |- ( ( 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 ) ) )
2726ralbidva 2839 . . . . . . 7 |- ( 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 ) ) )
2827rexbiia 2904 . . . . . 6 |- ( 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 ) )
2928imbi2i 310 . . . . 5 |- ( ( 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 ) ) )
3029ralbii 2834 . . . 4 |- ( 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 ) ) )
3130a1i 11 . . 3 |- ( 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 ) ) ) )
3217, 313anbi13d 1303 . 2 |- ( 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 ) ) ) ) )
33 lmres.5 . . 3 |- ( ph -> M e. ZZ )
341, 18, 33lmbr2 20051 . 2 |- ( 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 ) ) ) ) )
351, 18, 33lmbr2 20051 . 2 |- ( 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 ) ) ) ) )
3632, 34, 353bitr4rd 286 1 |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~> t ` J ) P ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 974   e. wcel 1842   A.wral 2753   E.wrex 2754   _Vcvv 3058   C_ wss 3413   class class class wbr 4394   dom cdm 4822   |` cres 4824   ` cfv 5568  (class class class)co 6277   ^pm cpm 7457   CCcc 9519   ZZcz 10904   ZZ>=cuz 11126  TopOnctopon 19685   ~~> tclm 20018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-cnex 9577  ax-resscn 9578  ax-pre-lttri 9595  ax-pre-lttrn 9596
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-po 4743  df-so 4744  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-1st 6783  df-2nd 6784  df-er 7347  df-pm 7459  df-en 7554  df-dom 7555  df-sdom 7556  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-neg 9843  df-z 10905  df-uz 11127  df-top 19689  df-topon 19692  df-lm 20021
This theorem is referenced by:  esumcvg  28519
  Copyright terms: Public domain W3C validator