Theorem fsumshft 7031

Description: Index shift of a finite sum.

Assertion

Ref	Expression
fsumshft	|- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_k e. ((M + K)...(N + K))[_(k - K) / j]_A)

Distinct variable groups:   A,k   j,k,K   j,M,k   j,N,k

Proof of Theorem fsumshft

Step	Hyp	Ref	Expression
1		0z 6146	. . . 4 |- 0 e. ZZ
2		fsumrev 7029	. . . 4 |- ((N e. (ZZ>` M) /\ 0 e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A)
3	1, 2	mp3an2 904	. . 3 |- ((N e. (ZZ>` M) /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A)
4	3	3adant2 798	. 2 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_j e. (M...N)A = sum_m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A)
5		fsumrev 7029	. . 3 |- (((0 - M) e. (ZZ>` (0 - N)) /\ K e. ZZ /\ A.m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A e. CC) -> sum_m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A = sum_k e. ((K - (0 - M))...(K - (0 - N)))[_(K - k) / m]_[_(0 - m) / j]_A)
6		uznegit 6429	. . . . 5 |- (N e. (ZZ>` M) -> -uM e. (ZZ>` -uN))
7		df-neg 5358	. . . . . 6 |- -uM = (0 - M)
8		df-neg 5358	. . . . . . 7 |- -uN = (0 - N)
9	8	fveq2i 3727	. . . . . 6 |- (ZZ>` -uN) = (ZZ>` (0 - N))
10	7, 9	eleq12i 1539	. . . . 5 |- (-uM e. (ZZ>` -uN) <-> (0 - M) e. (ZZ>` (0 - N)))
11	6, 10	sylib 198	. . . 4 |- (N e. (ZZ>` M) -> (0 - M) e. (ZZ>` (0 - N)))
12	11	3ad2ant1 800	. . 3 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> (0 - M) e. (ZZ>` (0 - N)))
13		3simp2 789	. . 3 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> K e. ZZ)
14		fzrevralt 6519	. . . . . . . 8 |- ((M e. ZZ /\ N e. ZZ /\ 0 e. ZZ) -> (A.j e. (M...N)A e. CC <-> A.m e. ((0 - N)...(0 - M))[(0 - m) / j]A e. CC))
15	1, 14	mp3an3 905	. . . . . . 7 |- ((M e. ZZ /\ N e. ZZ) -> (A.j e. (M...N)A e. CC <-> A.m e. ((0 - N)...(0 - M))[(0 - m) / j]A e. CC))
16		eluzel2 6424	. . . . . . 7 |- (N e. (ZZ>` M) -> M e. ZZ)
17		eluzelz 6423	. . . . . . 7 |- (N e. (ZZ>` M) -> N e. ZZ)
18	15, 16, 17	sylanc 471	. . . . . 6 |- (N e. (ZZ>` M) -> (A.j e. (M...N)A e. CC <-> A.m e. ((0 - N)...(0 - M))[(0 - m) / j]A e. CC))
19		oprex 3983	. . . . . . . 8 |- (0 - m) e. V
20		sbcel1g 2013	. . . . . . . 8 |- ((0 - m) e. V -> ([(0 - m) / j]A e. CC <-> [_(0 - m) / j]_A e. CC))
21	19, 20	ax-mp 7	. . . . . . 7 |- ([(0 - m) / j]A e. CC <-> [_(0 - m) / j]_A e. CC)
22	21	ralbii 1667	. . . . . 6 |- (A.m e. ((0 - N)...(0 - M))[(0 - m) / j]A e. CC <-> A.m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A e. CC)
23	18, 22	syl6bb 536	. . . . 5 |- (N e. (ZZ>` M) -> (A.j e. (M...N)A e. CC <-> A.m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A e. CC))
24	23	biimpa 416	. . . 4 |- ((N e. (ZZ>` M) /\ A.j e. (M...N)A e. CC) -> A.m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A e. CC)
25	24	3adant2 798	. . 3 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> A.m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A e. CC)
26	5, 12, 13, 25	syl3anc 858	. 2 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> sum_m e. ((0 - N)...(0 - M))[_(0 - m) / j]_A = sum_k e. ((K - (0 - M))...(K - (0 - N)))[_(K - k) / m]_[_(0 - m) / j]_A)
27		subnegt 5394	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (K + M))
28		axaddcom 5275	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K + M) = (M + K))
29	27, 28	eqtrd 1507	. . . . . . . . 9 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (M + K))
30	7	opreq2i 3972	. . . . . . . . 9 |- (K - -uM) = (K - (0 - M))
31	29, 30	syl5eqr 1521	. . . . . . . 8 |- ((K e. CC /\ M e. CC) -> (K - (0 - M)) = (M + K))
32	31	adantrr 395	. . . . . . 7 |- ((K e. CC /\ (M e. CC /\ N e. CC)) -> (K - (0 - M)) = (M + K))
33		subnegt 5394	. . . . . . . . . 10 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (K + N))
34		axaddcom 5275	. . . . . . . . . 10 |- ((K e. CC /\ N e. CC) -> (K + N) = (N + K))
35	33, 34	eqtrd 1507	. . . . . . . . 9 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (N + K))
36	8	opreq2i 3972	. . . . . . . . 9 |- (K - -uN) = (K - (0 - N))
37	35, 36	syl5eqr 1521	. . . . . . . 8 |- ((K e. CC /\ N e. CC) -> (K - (0 - N)) = (N + K))
38	37	adantrl 394	. . . . . . 7 |- ((K e. CC /\ (M e. CC /\ N e. CC)) -> (K - (0 - N)) = (N + K))
39	32, 38	opreq12d 3978	. . . . . 6 |- ((K e. CC /\ (M e. CC /\ N e. CC)) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
40		zcnt 6140	. . . . . 6 |- (K e. ZZ -> K e. CC)
41		zcnt 6140	. . . . . . . 8 |- (M e. ZZ -> M e. CC)
42	16, 41	syl 10	. . . . . . 7 |- (N e. (ZZ>` M) -> M e. CC)
43		zcnt 6140	. . . . . . . 8 |- (N e. ZZ -> N e. CC)
44	17, 43	syl 10	. . . . . . 7 |- (N e. (ZZ>` M) -> N e. CC)
45	42, 44	jca 288	. . . . . 6 |- (N e. (ZZ>` M) -> (M e. CC /\ N e. CC))
46	39, 40, 45	syl2an 454	. . . . 5 |- ((K e. ZZ /\ N e. (ZZ>` M)) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
47	46	ancoms 436	. . . 4 |- ((N e. (ZZ>` M) /\ K e. ZZ) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
48		negsubdi2t 5458	. . . . . . . . . 10 |- ((K e. CC /\ k e. CC) -> -u(K - k) = (k - K))
49		zcnt 6140	. . . . . . . . . 10 |- (k e. ZZ -> k e. CC)
50	48, 40, 49	syl2an 454	. . . . . . . . 9 |- ((K e. ZZ /\ k e. ZZ) -> -u(K - k) = (k - K))
51		df-neg 5358	. . . . . . . . 9 |- -u(K - k) = (0 - (K - k))
52	50, 51	syl5eqr 1521	. . . . . . . 8 |- ((K e. ZZ /\ k e. ZZ) -> (0 - (K - k)) = (k - K))
53	52	csbeq1d 2004	. . . . . . 7 |- ((K e. ZZ /\ k e. ZZ) -> [_(0 - (K - k)) / j]_A = [_(k - K) / j]_A)
54		oprex 3983	. . . . . . . 8 |- (K - k) e. V
55	19	ax-gen 963	. . . . . . . 8 |- A.m(0 - m) e. V
56		opreq2 3969	. . . . . . . . 9 |- (m = (K - k) -> (0 - m) = (0 - (K - k)))
57	56	csbco3g 2040	. . . . . . . 8 |- (((K - k) e. V /\ A.m(0 - m) e. V) -> [_(K - k) / m]_[_(0 - m) / j]_A = [_(0 - (K - k)) / j]_A)
58	54, 55, 57	mp2an 697	. . . . . . 7 |- [_(K - k) / m]_[_(0 - m) / j]_A = [_(0 - (K - k)) / j]_A
59	53, 58	syl5eq 1519	. . . . . 6 |- ((K e. ZZ /\ k e. ZZ) -> [_(K - k) / m]_