Theorem climshftlemg 10744

Description: A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)

Assertion

Ref	Expression
climshftlemg	|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A -> ( F shift M ) ~~> A ) )

Proof of Theorem climshftlemg

Dummy variables k m n x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zaddcl 8844	. . . . . . . 8 |- ( ( k e. ZZ /\ M e. ZZ ) -> ( k + M ) e. ZZ )
2	1	ancoms 265	. . . . . . 7 |- ( ( M e. ZZ /\ k e. ZZ ) -> ( k + M ) e. ZZ )
3	2	adantlr 462	. . . . . 6 |- ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) -> ( k + M ) e. ZZ )
4		eluzsub 9102	. . . . . . . . . . . 12 |- ( ( k e. ZZ /\ M e. ZZ /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
5	4	3com12 1148	. . . . . . . . . . 11 |- ( ( M e. ZZ /\ k e. ZZ /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
6	5	3expa 1144	. . . . . . . . . 10 |- ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( n - M ) e. ( ZZ>= ` k ) )
7		fveq2 5318	. . . . . . . . . . . . 13 |- ( m = ( n - M ) -> ( F ` m ) = ( F ` ( n - M ) ) )
8	7	eleq1d 2157	. . . . . . . . . . . 12 |- ( m = ( n - M ) -> ( ( F ` m ) e. CC <-> ( F ` ( n - M ) ) e. CC ) )
9	7	oveq1d 5681	. . . . . . . . . . . . . 14 |- ( m = ( n - M ) -> ( ( F ` m ) - A ) = ( ( F ` ( n - M ) ) - A ) )
10	9	fveq2d 5322	. . . . . . . . . . . . 13 |- ( m = ( n - M ) -> ( abs ` ( ( F ` m ) - A ) ) = ( abs ` ( ( F ` ( n - M ) ) - A ) ) )
11	10	breq1d 3861	. . . . . . . . . . . 12 |- ( m = ( n - M ) -> ( ( abs ` ( ( F ` m ) - A ) ) < x <-> ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) )
12	8, 11	anbi12d 458	. . . . . . . . . . 11 |- ( m = ( n - M ) -> ( ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
13	12	rspcv 2719	. . . . . . . . . 10 |- ( ( n - M ) e. ( ZZ>= ` k ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
14	6, 13	syl 14	. . . . . . . . 9 |- ( ( ( M e. ZZ /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
15	14	adantllr 466	. . . . . . . 8 |- ( ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
16		simplr 498	. . . . . . . . . 10 |- ( ( ( M e. ZZ /\ F e. V ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> F e. V )
17		zcn 8809	. . . . . . . . . . 11 |- ( M e. ZZ -> M e. CC )
18	17	ad2antrr 473	. . . . . . . . . 10 |- ( ( ( M e. ZZ /\ F e. V ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> M e. CC )
19		eluzelcn 9084	. . . . . . . . . . 11 |- ( n e. ( ZZ>= ` ( k + M ) ) -> n e. CC )
20	19	adantl 272	. . . . . . . . . 10 |- ( ( ( M e. ZZ /\ F e. V ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> n e. CC )
21		shftvalg 10324	. . . . . . . . . . . 12 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( ( F shift M ) ` n ) = ( F ` ( n - M ) ) )
22	21	eleq1d 2157	. . . . . . . . . . 11 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( ( ( F shift M ) ` n ) e. CC <-> ( F ` ( n - M ) ) e. CC ) )
23	21	oveq1d 5681	. . . . . . . . . . . . 13 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( ( ( F shift M ) ` n ) - A ) = ( ( F ` ( n - M ) ) - A ) )
24	23	fveq2d 5322	. . . . . . . . . . . 12 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( abs ` ( ( ( F shift M ) ` n ) - A ) ) = ( abs ` ( ( F ` ( n - M ) ) - A ) ) )
25	24	breq1d 3861	. . . . . . . . . . 11 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x <-> ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) )
26	22, 25	anbi12d 458	. . . . . . . . . 10 |- ( ( F e. V /\ M e. CC /\ n e. CC ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
27	16, 18, 20, 26	syl3anc 1175	. . . . . . . . 9 |- ( ( ( M e. ZZ /\ F e. V ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
28	27	adantlr 462	. . . . . . . 8 |- ( ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> ( ( F ` ( n - M ) ) e. CC /\ ( abs ` ( ( F ` ( n - M ) ) - A ) ) < x ) ) )
29	15, 28	sylibrd 168	. . . . . . 7 |- ( ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) /\ n e. ( ZZ>= ` ( k + M ) ) ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
30	29	ralrimdva 2454	. . . . . 6 |- ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
31		fveq2 5318	. . . . . . . 8 |- ( m = ( k + M ) -> ( ZZ>= ` m ) = ( ZZ>= ` ( k + M ) ) )
32	31	raleqdv 2569	. . . . . . 7 |- ( m = ( k + M ) -> ( A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) <-> A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
33	32	rspcev 2723	. . . . . 6 |- ( ( ( k + M ) e. ZZ /\ A. n e. ( ZZ>= ` ( k + M ) ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) )
34	3, 30, 33	syl6an 1369	. . . . 5 |- ( ( ( M e. ZZ /\ F e. V ) /\ k e. ZZ ) -> ( A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
35	34	rexlimdva 2490	. . . 4 |- ( ( M e. ZZ /\ F e. V ) -> ( E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
36	35	ralimdv 2443	. . 3 |- ( ( M e. ZZ /\ F e. V ) -> ( A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) -> A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) )
37	36	anim2d 331	. 2 |- ( ( M e. ZZ /\ F e. V ) -> ( ( A e. CC /\ A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) ) -> ( A e. CC /\ A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) ) )
38		simpr 109	. . 3 |- ( ( M e. ZZ /\ F e. V ) -> F e. V )
39		eqidd 2090	. . 3 |- ( ( ( M e. ZZ /\ F e. V ) /\ m e. ZZ ) -> ( F ` m ) = ( F ` m ) )
40	38, 39	clim 10723	. 2 |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. k e. ZZ A. m e. ( ZZ>= ` k ) ( ( F ` m ) e. CC /\ ( abs ` ( ( F ` m ) - A ) ) < x ) ) ) )
41		ovshftex 10307	. . . . 5 |- ( ( F e. V /\ M e. CC ) -> ( F shift M ) e. _V )
42	41	ancoms 265	. . . 4 |- ( ( M e. CC /\ F e. V ) -> ( F shift M ) e. _V )
43	17, 42	sylan 278	. . 3 |- ( ( M e. ZZ /\ F e. V ) -> ( F shift M ) e. _V )
44		eqidd 2090	. . 3 |- ( ( ( M e. ZZ /\ F e. V ) /\ n e. ZZ ) -> ( ( F shift M ) ` n ) = ( ( F shift M ) ` n ) )
45	43, 44	clim 10723	. 2 |- ( ( M e. ZZ /\ F e. V ) -> ( ( F shift M ) ~~> A <-> ( A e. CC /\ A. x e. RR+ E. m e. ZZ A. n e. ( ZZ>= ` m ) ( ( ( F shift M ) ` n ) e. CC /\ ( abs ` ( ( ( F shift M ) ` n ) - A ) ) < x ) ) ) )
46	37, 40, 45	3imtr4d 202	1 |- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A -> ( F shift M ) ~~> A ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 925   = wceq 1290   e. wcel 1439   A.wral 2360   E.wrex 2361   _Vcvv 2620   class class class wbr 3851   ` cfv 5028  (class class class)co 5666   CCcc 7402   + caddc 7407   < clt 7576   - cmin 7707   ZZcz 8804   ZZ>=cuz 9073   RR+crp 9188   shift cshi 10302   abscabs 10484   ~~> cli 10720

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3960  ax-sep 3963  ax-pow 4015  ax-pr 4045  ax-un 4269  ax-setind 4366  ax-cnex 7490  ax-resscn 7491  ax-1cn 7492  ax-1re 7493  ax-icn 7494  ax-addcl 7495  ax-addrcl 7496  ax-mulcl 7497  ax-addcom 7499  ax-addass 7501  ax-distr 7503  ax-i2m1 7504  ax-0lt1 7505  ax-0id 7507  ax-rnegex 7508  ax-cnre 7510  ax-pre-ltirr 7511  ax-pre-ltwlin 7512  ax-pre-lttrn 7513  ax-pre-ltadd 7515

This theorem depends on definitions:  df-bi 116  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-nel 2352  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2622  df-sbc 2842  df-csb 2935  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-uni 3660  df-int 3695  df-iun 3738  df-br 3852  df-opab 3906  df-mpt 3907  df-id 4129  df-xp 4457  df-rel 4458  df-cnv 4459  df-co 4460  df-dm 4461  df-rn 4462  df-res 4463  df-ima 4464  df-iota 4993  df-fun 5030  df-fn 5031  df-f 5032  df-f1 5033  df-fo 5034  df-f1o 5035  df-fv 5036  df-riota 5622  df-ov 5669  df-oprab 5670  df-mpt2 5671  df-pnf 7578  df-mnf 7579  df-xr 7580  df-ltxr 7581  df-le 7582  df-sub 7709  df-neg 7710  df-inn 8477  df-n0 8728  df-z 8805  df-uz 9074  df-shft 10303  df-clim 10721

This theorem is referenced by:  climshft  10746