Theorem lmres 20314

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.

Step	Hyp	Ref	Expression
1		lmres.2	. . . . . . 7 |- ( ph -> J e. (TopOn ` X ) )
2		toponmax 19941	. . . . . . 7 |- ( J e. (TopOn ` X ) -> X e. J )
3	1, 2	syl 17	. . . . . 6 |- ( ph -> X e. J )
4		cnex 9627	. . . . . 6 |- CC e. _V
5		ssid 3483	. . . . . . 7 |- X C_ X
6		uzssz 11185	. . . . . . . 8 |- ( ZZ>= ` M ) C_ ZZ
7		zsscn 10952	. . . . . . . 8 |- ZZ C_ CC
8	6, 7	sstri 3473	. . . . . . 7 |- ( ZZ>= ` M ) C_ CC
9		pmss12g 7509	. . . . . . 7 |- ( ( ( X C_ X /\ ( ZZ>= ` M ) C_ CC ) /\ ( X e. J /\ CC e. _V ) ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
10	5, 8, 9	mpanl12 686	. . . . . 6 |- ( ( X e. J /\ CC e. _V ) -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
11	3, 4, 10	sylancl 666	. . . . 5 |- ( ph -> ( X ^pm ( ZZ>= ` M ) ) C_ ( X ^pm CC ) )
12		fvex 5891	. . . . . 6 |- ( ZZ>= ` M ) e. _V
13		lmres.4	. . . . . 6 |- ( ph -> F e. ( X ^pm CC ) )
14		pmresg 7510	. . . . . 6 |- ( ( ( ZZ>= ` M ) e. _V /\ F e. ( X ^pm CC ) ) -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
15	12, 13, 14	sylancr 667	. . . . 5 |- ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm ( ZZ>= ` M ) ) )
16	11, 15	sseldd 3465	. . . 4 |- ( ph -> ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) )
17	16, 13	2thd 243	. . 3 |- ( ph -> ( ( F |` ( ZZ>= ` M ) ) e. ( X ^pm CC ) <-> F e. ( X ^pm CC ) ) )
18		eqid 2422	. . . . . . . . . 10 |- ( ZZ>= ` M ) = ( ZZ>= ` M )
19	18	uztrn2 11183	. . . . . . . . 9 |- ( ( j e. ( ZZ>= ` M ) /\ k e. ( ZZ>= ` j ) ) -> k e. ( ZZ>= ` M ) )
20		dmres 5144	. . . . . . . . . . . 12 |- dom ( F |` ( ZZ>= ` M ) ) = ( ( ZZ>= ` M ) i^i dom F )
21	20	elin2 3653	. . . . . . . . . . 11 |- ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> ( k e. ( ZZ>= ` M ) /\ k e. dom F ) )
22	21	baib 911	. . . . . . . . . 10 |- ( k e. ( ZZ>= ` M ) -> ( k e. dom ( F |` ( ZZ>= ` M ) ) <-> k e. dom F ) )
23		fvres 5895	. . . . . . . . . . 11 |- ( k e. ( ZZ>= ` M ) -> ( ( F |` ( ZZ>= ` M ) ) ` k ) = ( F ` k ) )
24	23	eleq1d 2491	. . . . . . . . . 10 |- ( k e. ( ZZ>= ` M ) -> ( ( ( F |` ( ZZ>= ` M ) ) ` k ) e. u <-> ( F ` k ) e. u ) )
25	22, 24	anbi12d 715	. . . . . . . . 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 ) ) )
26	19, 25	syl 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 ) ) )
27	26	ralbidva 2858	. . . . . . 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 ) ) )
28	27	rexbiia 2923	. . . . . 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 ) )
29	28	imbi2i 313	. . . . 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 ) ) )
30	29	ralbii 2853	. . . 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 ) ) )
31	30	a1i 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 ) ) ) )
32	17, 31	3anbi13d 1337	. 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 )
34	1, 18, 33	lmbr2 20273	. 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 ) ) ) ) )
35	1, 18, 33	lmbr2 20273	. 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 ) ) ) ) )
36	32, 34, 35	3bitr4rd 289	1 |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~> t ` J ) P ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   e. wcel 1872   A.wral 2771   E.wrex 2772   _Vcvv 3080   C_ wss 3436   class class class wbr 4423   dom cdm 4853   |` cres 4855   ` cfv 5601  (class class class)co 6305   ^pm cpm 7484   CCcc 9544   ZZcz 10944   ZZ>=cuz 11166  TopOnctopon 19916   ~~> tclm 20240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-cnex 9602  ax-resscn 9603  ax-pre-lttri 9620  ax-pre-lttrn 9621

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-1st 6807  df-2nd 6808  df-er 7374  df-pm 7486  df-en 7581  df-dom 7582  df-sdom 7583  df-pnf 9684  df-mnf 9685  df-xr 9686  df-ltxr 9687  df-le 9688  df-neg 9870  df-z 10945  df-uz 11167  df-top 19919  df-topon 19921  df-lm 20243

This theorem is referenced by:  esumcvg  28915