Theorem iserzshft2 7107

Description: Index shift of an infinite series. (Contributed by Paul Chapman, 19-Nov-2007.)

Hypotheses

Ref	Expression
iserzshft2.1	|- F e. V
iserzshft2.2	|- G e. V
iserzshft2.3	|- M e. ZZ
iserzshft2.4	|- K e. ZZ

Assertion

Ref	Expression
iserzshft2	|- ((A e. B /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) -> ((<.M, + >. seq F) ~~> A <-> (<.(M + K), + >. seq G) ~~> A))

Distinct variable groups:   k,F   k,G   k,K   k,M

Proof of Theorem iserzshft2

Step	Hyp	Ref	Expression
1		climcl 6978	. . . 4 |- ((A e. B /\ (<.M, + >. seq F) ~~> A) -> A e. CC)
2	1	anim1i 334	. . 3 |- (((A e. B /\ (<.M, + >. seq F) ~~> A) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) -> (A e. CC /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))))
3	2	an1rs 491	. 2 |- (((A e. B /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) /\ (<.M, + >. seq F) ~~> A) -> (A e. CC /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))))
4		climcl 6978	. . . 4 |- ((A e. B /\ (<.(M + K), + >. seq G) ~~> A) -> A e. CC)
5	4	anim1i 334	. . 3 |- (((A e. B /\ (<.(M + K), + >. seq G) ~~> A) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) -> (A e. CC /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))))
6	5	an1rs 491	. 2 |- (((A e. B /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) /\ (<.(M + K), + >. seq G) ~~> A) -> (A e. CC /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))))
7		breq2 2628	. . . . . 6 |- (A = if(A e. CC, A, 0) -> ((<.M, + >. seq F) ~~> A <-> (<.M, + >. seq F) ~~> if(A e. CC, A, 0)))
8		breq2 2628	. . . . . 6 |- (A = if(A e. CC, A, 0) -> ((<.(M + K), + >. seq G) ~~> A <-> (<.(M + K), + >. seq G) ~~> if(A e. CC, A, 0)))
9	7, 8	bibi12d 631	. . . . 5 |- (A = if(A e. CC, A, 0) -> (((<.M, + >. seq F) ~~> A <-> (<.(M + K), + >. seq G) ~~> A) <-> ((<.M, + >. seq F) ~~> if(A e. CC, A, 0) <-> (<.(M + K), + >. seq G) ~~> if(A e. CC, A, 0))))
10	9	imbi2d 614	. . . 4 |- (A = if(A e. CC, A, 0) -> ((A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> ((<.M, + >. seq F) ~~> A <-> (<.(M + K), + >. seq G) ~~> A)) <-> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> ((<.M, + >. seq F) ~~> if(A e. CC, A, 0) <-> (<.(M + K), + >. seq G) ~~> if(A e. CC, A, 0)))))
11		iserzshft2.4	. . . . . . . . . . 11 |- K e. ZZ
12		fsumshft 7031	. . . . . . . . . . 11 |- ((m e. (ZZ>` M) /\ K e. ZZ /\ A.k e. (M...m)(F` k) e. CC) -> sum_k e. (M...m)(F` k) = sum_n e. ((M + K)...(m + K))[_(n - K) / k]_(F` k))
13	11, 12	mp3an2 906	. . . . . . . . . 10 |- ((m e. (ZZ>` M) /\ A.k e. (M...m)(F` k) e. CC) -> sum_k e. (M...m)(F` k) = sum_n e. ((M + K)...(m + K))[_(n - K) / k]_(F` k))
14		r19.26 1753	. . . . . . . . . . . 12 |- (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) <-> (A.k e. (ZZ>` M)(F` k) e. CC /\ A.k e. (ZZ>` M)(G` (k + K)) = (F` k)))
15	14	pm3.26bi 322	. . . . . . . . . . 11 |- (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> A.k e. (ZZ>` M)(F` k) e. CC)
16		elfzuzt 6489	. . . . . . . . . . . . 13 |- (k e. (M...m) -> k e. (ZZ>` M))
17	16	imim1i 16	. . . . . . . . . . . 12 |- ((k e. (ZZ>` M) -> (F` k) e. CC) -> (k e. (M...m) -> (F` k) e. CC))
18	17	r19.20i2 1706	. . . . . . . . . . 11 |- (A.k e. (ZZ>` M)(F` k) e. CC -> A.k e. (M...m)(F` k) e. CC)
19	15, 18	syl 10	. . . . . . . . . 10 |- (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> A.k e. (M...m)(F` k) e. CC)
20	13, 19	sylan2 453	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k))) -> sum_k e. (M...m)(F` k) = sum_n e. ((M + K)...(m + K))[_(n - K) / k]_(F` k))
21		eluzelz 6424	. . . . . . . . . . . . . . . . . 18 |- (n e. (ZZ>` (M + K)) -> n e. ZZ)
22		zcnt 6142	. . . . . . . . . . . . . . . . . 18 |- (n e. ZZ -> n e. CC)
23	21, 22	syl 10	. . . . . . . . . . . . . . . . 17 |- (n e. (ZZ>` (M + K)) -> n e. CC)
24	11	zre 6143	. . . . . . . . . . . . . . . . . . 19 |- K e. RR
25	24	recn 5326	. . . . . . . . . . . . . . . . . 18 |- K e. CC
26		npcant 5411	. . . . . . . . . . . . . . . . . 18 |- ((n e. CC /\ K e. CC) -> ((n - K) + K) = n)
27	25, 26	mpan2 698	. . . . . . . . . . . . . . . . 17 |- (n e. CC -> ((n - K) + K) = n)
28	23, 27	syl 10	. . . . . . . . . . . . . . . 16 |- (n e. (ZZ>` (M + K)) -> ((n - K) + K) = n)
29	28	fveq2d 3734	. . . . . . . . . . . . . . 15 |- (n e. (ZZ>` (M + K)) -> (G` ((n - K) + K)) = (G` n))
30	29	adantl 390	. . . . . . . . . . . . . 14 |- ((A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) /\ n e. (ZZ>` (M + K))) -> (G` ((n - K) + K)) = (G` n))
31		iserzshft2.3	. . . . . . . . . . . . . . . . . 18 |- M e. ZZ
32	31, 11	eluzsubi 6438	. . . . . . . . . . . . . . . . 17 |- (n e. (ZZ>` (M + K)) -> (n - K) e. (ZZ>` M))
33		fveq2 3730	. . . . . . . . . . . . . . . . . . . 20 |- (k = (n - K) -> (F` k) = (F` (n - K)))
34	33	eleq1d 1543	. . . . . . . . . . . . . . . . . . 19 |- (k = (n - K) -> ((F` k) e. CC <-> (F` (n - K)) e. CC))
35		opreq1 3974	. . . . . . . . . . . . . . . . . . . . 21 |- (k = (n - K) -> (k + K) = ((n - K) + K))
36	35	fveq2d 3734	. . . . . . . . . . . . . . . . . . . 20 |- (k = (n - K) -> (G` (k + K)) = (G` ((n - K) + K)))
37	36, 33	eqeq12d 1492	. . . . . . . . . . . . . . . . . . 19 |- (k = (n - K) -> ((G` (k + K)) = (F` k) <-> (G` ((n - K) + K)) = (F` (n - K))))
38	34, 37	anbi12d 630	. . . . . . . . . . . . . . . . . 18 |- (k = (n - K) -> (((F` k) e. CC /\ (G` (k + K)) = (F` k)) <-> ((F` (n - K)) e. CC /\ (G` ((n - K) + K)) = (F` (n - K)))))
39	38	rcla4v 1876	. . . . . . . . . . . . . . . . 17 |- ((n - K) e. (ZZ>` M) -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> ((F` (n - K)) e. CC /\ (G` ((n - K) + K)) = (F` (n - K)))))
40	32, 39	syl 10	. . . . . . . . . . . . . . . 16 |- (n e. (ZZ>` (M + K)) -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` (k + K)) = (F` k)) -> ((F` (n - K)) e. CC /\