Theorem climshft 7104

Description: A shifted function converges iff the original function converges.

Hypotheses

Ref	Expression
climshft.1	|- F e. V
climshft.2	|- M e. ZZ

Assertion

Ref	Expression
climshft	|- (A e. CC -> ((F shift M) ~~> A <-> F ~~> A))

Proof of Theorem climshft

Step	Hyp	Ref	Expression
1		0z 6148	. . . 4 |- 0 e. ZZ
2		uzssz 6431	. . . 4 |- (ZZ>` 0) (_ ZZ
3		ssid 2083	. . . 4 |- ZZ (_ ZZ
4		oprex 3989	. . . 4 |- (F shift M) e. V
5	1, 2, 3, 1, 2, 3, 4	clm2 7078	. . 3 |- (A e. CC -> ((F shift M) ~~> A <-> A.x e. RR (0 < x -> E.j e. ZZ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x)))))
6		climshft.2	. . . . . . . . . . . . . . . . . . 19 |- M e. ZZ
7	6	zre 6143	. . . . . . . . . . . . . . . . . 18 |- M e. RR
8		lesubaddt 5641	. . . . . . . . . . . . . . . . . 18 |- ((j e. RR /\ M e. RR /\ n e. RR) -> ((j - M) <_ n <-> j <_ (n + M)))
9	7, 8	mp3an2 906	. . . . . . . . . . . . . . . . 17 |- ((j e. RR /\ n e. RR) -> ((j - M) <_ n <-> j <_ (n + M)))
10		zret 6141	. . . . . . . . . . . . . . . . 17 |- (j e. ZZ -> j e. RR)
11		zret 6141	. . . . . . . . . . . . . . . . 17 |- (n e. ZZ -> n e. RR)
12	9, 10, 11	syl2an 456	. . . . . . . . . . . . . . . 16 |- ((j e. ZZ /\ n e. ZZ) -> ((j - M) <_ n <-> j <_ (n + M)))
13	12	adantr 391	. . . . . . . . . . . . . . 15 |- (((j e. ZZ /\ n e. ZZ) /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) -> ((j - M) <_ n <-> j <_ (n + M)))
14		zaddclt 6167	. . . . . . . . . . . . . . . . . . 19 |- ((n e. ZZ /\ M e. ZZ) -> (n + M) e. ZZ)
15	6, 14	mpan2 698	. . . . . . . . . . . . . . . . . 18 |- (n e. ZZ -> (n + M) e. ZZ)
16		breq2 2628	. . . . . . . . . . . . . . . . . . . 20 |- (t = (n + M) -> (j <_ t <-> j <_ (n + M)))
17		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (n + M) -> ((F shift M)` t) = ((F shift M)` (n + M)))
18	17	eleq1d 1543	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (n + M) -> (((F shift M)` t) e. CC <-> ((F shift M)` (n + M)) e. CC))
19	17	opreq1d 3981	. . . . . . . . . . . . . . . . . . . . . . 23 |- (t = (n + M) -> (((F shift M)` t) - A) = (((F shift M)` (n + M)) - A))
20	19	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . 22 |- (t = (n + M) -> (abs` (((F shift M)` t) - A)) = (abs` (((F shift M)` (n + M)) - A)))
21	20	breq1d 2634	. . . . . . . . . . . . . . . . . . . . 21 |- (t = (n + M) -> ((abs` (((F shift M)` t) - A)) < x <-> (abs` (((F shift M)` (n + M)) - A)) < x))
22	18, 21	anbi12d 630	. . . . . . . . . . . . . . . . . . . 20 |- (t = (n + M) -> ((((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x) <-> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x)))
23	16, 22	imbi12d 628	. . . . . . . . . . . . . . . . . . 19 |- (t = (n + M) -> ((j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x)) <-> (j <_ (n + M) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x))))
24	23	rcla4v 1876	. . . . . . . . . . . . . . . . . 18 |- ((n + M) e. ZZ -> (A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x)) -> (j <_ (n + M) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x))))
25	15, 24	syl 10	. . . . . . . . . . . . . . . . 17 |- (n e. ZZ -> (A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x)) -> (j <_ (n + M) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x))))
26	25	imp 350	. . . . . . . . . . . . . . . 16 |- ((n e. ZZ /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) -> (j <_ (n + M) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x)))
27	26	adantll 394	. . . . . . . . . . . . . . 15 |- (((j e. ZZ /\ n e. ZZ) /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) -> (j <_ (n + M) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x)))
28	13, 27	sylbid 203	. . . . . . . . . . . . . 14 |- (((j e. ZZ /\ n e. ZZ) /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) -> ((j - M) <_ n -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x)))
29	28	imp 350	. . . . . . . . . . . . 13 |- ((((j e. ZZ /\ n e. ZZ) /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) /\ (j - M) <_ n) -> (((F shift M)` (n + M)) e. CC /\ (abs` (((F shift M)` (n + M)) - A)) < x))
30		zcnt 6142	. . . . . . . . . . . . . . . . . 18 |- ((n + M) e. ZZ -> (n + M) e. CC)
31		climshft.1	. . . . . . . . . . . . . . . . . . . 20 |- F e. V
32	31	shftvalt 6347	. . . . . . . . . . . . . . . . . . 19 |- ((M e. ZZ /\ (n + M) e. CC) -> ((F shift M)` (n + M)) = (F` ((n + M) - M)))
33	6, 32	mpan 697	. . . . . . . . . . . . . . . . . 18 |- ((n + M) e. CC -> ((F shift M)` (n + M)) = (F` ((n + M) - M)))
34	15, 30, 33	3syl 20	. . . . . . . . . . . . . . . . 17 |- (n e. ZZ -> ((F shift M)` (n + M)) = (F` ((n + M) - M)))
35		zcnt 6142	. . . . . . . . . . . . . . . . . . 19 |- (n e. ZZ -> n e. CC)
36	7	recn 5326	. . . . . . . . . . . . . . . . . . . 20 |- M e. CC
37		pncant 5409	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. CC /\ M e. CC) -> ((n + M) - M) = n)
38	36, 37	mpan2 698	. . . . . . . . . . . . . . . . . . 19 |- (n e. CC -> ((n + M) - M) = n)
39	35, 38	syl 10	. . . . . . . . . . . . . . . . . 18 |- (n e. ZZ -> ((n + M) - M) = n)
40	39	fveq2d 3734	. . . . . . . . . . . . . . . . 17 |- (n e. ZZ -> (F` ((n + M) - M)) = (F` n))
41	34, 40	eqtr2d 1511	. . . . . . . . . . . . . . . 16 |- (n e. ZZ -> (F` n) = ((F shift M)` (n + M)))
42	41	adantl 390	. . . . . . . . . . . . . . 15 |- ((j e. ZZ /\ n e. ZZ) -> (F` n) = ((F shift M)` (n + M)))
43	42	ad2antrr 406	. . . . . . . . . . . . . 14 |- ((((j e. ZZ /\ n e. ZZ) /\ A.t e. ZZ (j <_ t -> (((F shift M)` t) e. CC /\ (abs` (((F shift M)` t) - A)) < x))) /\ (j - M) <_ n) -> (F` n) = ((F shift M)` (n + M)))
44		eleq1 1537	. . . . . . . . . . . . . . 15 |- ((F` n) = ((F shift M)` (n + M)) -> ((F` n) e. CC <-> ((F shift M)` (n + M)) e. CC))
45		opreq1 3974	. . . . . . . . . . . . . . . . 17 |- ((F` n) = ((F shift M)` (n + M)) -> ((F` n) - A) = (((F shift M)` (n + M)) - A))
46	45	fveq2d 3734	. . . . . . . . . . . . . . . 16 |- ((F` n) = ((F shift M)` (n + M)) -> (abs` ((F` n) - A)) = (abs` (((F shift M)` (n + M)) - A)))
47	46	breq1d 2634	. . . . . . . . . . . . . . 15 |- ((F` n) = ((F shift M)` (n + M)) -> ((abs` ((F` n) - A)) < x <-> (abs` (((F shift M)` (n + M)) - A)) < x))
48	44, 47	anbi12d 630	. . . . . . . . . . . . . 14 |- ((F` n)