Theorem fsumshft 6920

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 6044	. . . 4 |- 0 e. ZZ
2		fsumrev 6918	. . . 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 900	. . 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 795	. 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 6918	. . 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 6312	. . . . 5 |- (N e. (ZZ>` M) -> -uM e. (ZZ>` -uN))
7		df-neg 5281	. . . . . 6 |- -uM = (0 - M)
8		df-neg 5281	. . . . . . 7 |- -uN = (0 - N)
9	8	fveq2i 3666	. . . . . 6 |- (ZZ>` -uN) = (ZZ>` (0 - N))
10	7, 9	eleq12i 1515	. . . . 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 797	. . 3 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> (0 - M) e. (ZZ>` (0 - N)))
13		3simp2 786	. . 3 |- ((N e. (ZZ>` M) /\ K e. ZZ /\ A.j e. (M...N)A e. CC) -> K e. ZZ)
14		fzrevralt 6402	. . . . . . . 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 901	. . . . . . 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 6307	. . . . . . 7 |- (N e. (ZZ>` M) -> M e. ZZ)
17		eluzelz 6306	. . . . . . 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 3922	. . . . . . . 8 |- (0 - m) e. V
20		sbcel1g 1984	. . . . . . . 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 1643	. . . . . 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 534	. . . . 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 795	. . 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 855	. 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 5317	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (K + M))
28		axaddcom 5198	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K + M) = (M + K))
29	27, 28	eqtrd 1483	. . . . . . . . 9 |- ((K e. CC /\ M e. CC) -> (K - -uM) = (M + K))
30	7	opreq2i 3911	. . . . . . . . 9 |- (K - -uM) = (K - (0 - M))
31	29, 30	syl5eqr 1497	. . . . . . . 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 5317	. . . . . . . . . 10 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (K + N))
34		axaddcom 5198	. . . . . . . . . 10 |- ((K e. CC /\ N e. CC) -> (K + N) = (N + K))
35	33, 34	eqtrd 1483	. . . . . . . . 9 |- ((K e. CC /\ N e. CC) -> (K - -uN) = (N + K))
36	8	opreq2i 3911	. . . . . . . . 9 |- (K - -uN) = (K - (0 - N))
37	35, 36	syl5eqr 1497	. . . . . . . 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 3917	. . . . . 6 |- ((K e. CC /\ (M e. CC /\ N e. CC)) -> ((K - (0 - M))...(K - (0 - N))) = ((M + K)...(N + K)))
40		zcnt 6038	. . . . . 6 |- (K e. ZZ -> K e. CC)
41		zcnt 6038	. . . . . . . 8 |- (M e. ZZ -> M e. CC)
42	16, 41	syl 10	. . . . . . 7 |- (N e. (ZZ>` M) -> M e. CC)
43		zcnt 6038	. . . . . . . 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 5381	. . . . . . . . . 10 |- ((K e. CC /\ k e. CC) -> -u(K - k) = (k - K))
49		zcnt 6038	. . . . . . . . . 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 5281	. . . . . . . . 9 |- -u(K - k) = (0 - (K - k))
52	50, 51	syl5eqr 1497	. . . . . . . 8 |- ((K e. ZZ /\ k e. ZZ) -> (0 - (K - k)) = (k - K))
53	52	csbeq1d 1975	. . . . . . 7 |- ((K e. ZZ /\ k e. ZZ) -> [_(0 - (K - k)) / j]_A = [_(k - K) / j]_A)
54		oprex 3922	. . . . . . . 8 |- (K - k) e. V
55	19	ax-gen 955	. . . . . . . 8 |- A.m(0 - m) e. V
56		opreq2 3908	. . . . . . . . 9 |- (m = (K - k) -> (0 - m) = (0 - (K - k)))
57	56	csbco3g 2011	. . . . . . . 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 694	. . . . . . 7 |- [_(K - k) / m]_[_(0 - m) / j]_A = [_(0 - (K - k)) / j]_A
59	53, 58	syl5eq 1495	. . . . . 6 |- ((K e. ZZ /\ k e. ZZ) -> [_(K - k)