Theorem fsumrev 6967

Description: Reversal of a finite sum. Warning: The HTML proof page is 0.6 MB in size.

Assertion

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

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

Proof of Theorem fsumrev

Step	Hyp	Ref	Expression
1		nncant 5441	. . . . . . . . . 10 |- ((K e. CC /\ M e. CC) -> (K - (K - M)) = M)
2		zcnt 6087	. . . . . . . . . 10 |- (K e. ZZ -> K e. CC)
3		zcnt 6087	. . . . . . . . . 10 |- (M e. ZZ -> M e. CC)
4	1, 2, 3	syl2an 454	. . . . . . . . 9 |- ((K e. ZZ /\ M e. ZZ) -> (K - (K - M)) = M)
5	4	csbeq1d 1994	. . . . . . . 8 |- ((K e. ZZ /\ M e. ZZ) -> [_(K - (K - M)) / j]_A = [_M / j]_A)
6	5	adantr 389	. . . . . . 7 |- (((K e. ZZ /\ M e. ZZ) /\ A.j e. (M...M)A e. CC) -> [_(K - (K - M)) / j]_A = [_M / j]_A)
7		fzrevralt 6451	. . . . . . . . . . 11 |- ((M e. ZZ /\ M e. ZZ /\ K e. ZZ) -> (A.j e. (M...M)A e. CC <-> A.k e. ((K - M)...(K - M))[(K - k) / j]A e. CC))
8		pm3.27 323	. . . . . . . . . . 11 |- ((K e. ZZ /\ M e. ZZ) -> M e. ZZ)
9		pm3.26 319	. . . . . . . . . . 11 |- ((K e. ZZ /\ M e. ZZ) -> K e. ZZ)
10	7, 8, 8, 9	syl3anc 856	. . . . . . . . . 10 |- ((K e. ZZ /\ M e. ZZ) -> (A.j e. (M...M)A e. CC <-> A.k e. ((K - M)...(K - M))[(K - k) / j]A e. CC))
11		oprex 3968	. . . . . . . . . . . 12 |- (K - k) e. V
12		sbcel1g 2003	. . . . . . . . . . . 12 |- ((K - k) e. V -> ([(K - k) / j]A e. CC <-> [_(K - k) / j]_A e. CC))
13	11, 12	ax-mp 7	. . . . . . . . . . 11 |- ([(K - k) / j]A e. CC <-> [_(K - k) / j]_A e. CC)
14	13	ralbii 1659	. . . . . . . . . 10 |- (A.k e. ((K - M)...(K - M))[(K - k) / j]A e. CC <-> A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC)
15	10, 14	syl6bb 534	. . . . . . . . 9 |- ((K e. ZZ /\ M e. ZZ) -> (A.j e. (M...M)A e. CC <-> A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC))
16	15	biimpa 416	. . . . . . . 8 |- (((K e. ZZ /\ M e. ZZ) /\ A.j e. (M...M)A e. CC) -> A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC)
17		fsum1s 6947	. . . . . . . . . 10 |- (((K - M) e. ZZ /\ A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC) -> sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A = [_(K - M) / k]_[_(K - k) / j]_A)
18		oprex 3968	. . . . . . . . . . 11 |- (K - M) e. V
19	11	ax-gen 960	. . . . . . . . . . 11 |- A.k(K - k) e. V
20		opreq2 3954	. . . . . . . . . . . 12 |- (k = (K - M) -> (K - k) = (K - (K - M)))
21	20	csbco3g 2030	. . . . . . . . . . 11 |- (((K - M) e. V /\ A.k(K - k) e. V) -> [_(K - M) / k]_[_(K - k) / j]_A = [_(K - (K - M)) / j]_A)
22	18, 19, 21	mp2an 695	. . . . . . . . . 10 |- [_(K - M) / k]_[_(K - k) / j]_A = [_(K - (K - M)) / j]_A
23	17, 22	syl6eq 1515	. . . . . . . . 9 |- (((K - M) e. ZZ /\ A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC) -> sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A = [_(K - (K - M)) / j]_A)
24		zsubclt 6115	. . . . . . . . 9 |- ((K e. ZZ /\ M e. ZZ) -> (K - M) e. ZZ)
25	23, 24	sylan 448	. . . . . . . 8 |- (((K e. ZZ /\ M e. ZZ) /\ A.k e. ((K - M)...(K - M))[_(K - k) / j]_A e. CC) -> sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A = [_(K - (K - M)) / j]_A)
26	16, 25	syldan 467	. . . . . . 7 |- (((K e. ZZ /\ M e. ZZ) /\ A.j e. (M...M)A e. CC) -> sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A = [_(K - (K - M)) / j]_A)
27		fsum1s 6947	. . . . . . . 8 |- ((M e. ZZ /\ A.j e. (M...M)A e. CC) -> sum_j e. (M...M)A = [_M / j]_A)
28	27	adantll 392	. . . . . . 7 |- (((K e. ZZ /\ M e. ZZ) /\ A.j e. (M...M)A e. CC) -> sum_j e. (M...M)A = [_M / j]_A)
29	6, 26, 28	3eqtr4rd 1510	. . . . . 6 |- (((K e. ZZ /\ M e. ZZ) /\ A.j e. (M...M)A e. CC) -> sum_j e. (M...M)A = sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A)
30	29	anasss 440	. . . . 5 |- ((K e. ZZ /\ (M e. ZZ /\ A.j e. (M...M)A e. CC)) -> sum_j e. (M...M)A = sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A)
31	30	an1s 485	. . . 4 |- ((M e. ZZ /\ (K e. ZZ /\ A.j e. (M...M)A e. CC)) -> sum_j e. (M...M)A = sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A)
32	31	ex 373	. . 3 |- (M e. ZZ -> ((K e. ZZ /\ A.j e. (M...M)A e. CC) -> sum_j e. (M...M)A = sum_k e. ((K - M)...(K - M))[_(K - k) / j]_A))
33		fzssp1t 6438	. . . . . . . . . 10 |- ((M e. ZZ /\ n e. ZZ) -> (M...n) (_ (M...(n + 1)))
34		eluzel2 6356	. . . . . . . . . 10 |- (n e. (ZZ>` M) -> M e. ZZ)
35		eluzelz 6355	. . . . . . . . . 10 |- (n e. (ZZ>` M) -> n e. ZZ)
36	33, 34, 35	sylanc 471	. . . . . . . . 9 |- (n e. (ZZ>` M) -> (M...n) (_ (M...(n + 1)))
37	36	sseld 2057	. . . . . . . 8 |- (n e. (ZZ>` M) -> (j e. (M...n) -> j e. (M...(n + 1))))
38	37	imim1d 28	. . . . . . 7 |- (n e. (ZZ>` M) -> ((j e. (M...(n + 1)) -> A e. CC) -> (j e. (M...n) -> A e. CC)))
39	38	r19.20dv2 1703	. . . . . 6 |- (n e. (ZZ>` M) -> (A.j e. (M...(n + 1))A e. CC -> A.j e. (M...n)A e. CC))
40	39	anim2d 559	. . . . 5 |- (n e. (ZZ>` M) -> ((K e. ZZ /\ A.j e. (M...(n + 1))A e. CC) -> (K e. ZZ /\ A.j e. (M...n)A e. CC)))
41	40	imim1d 28	. . . 4 |- (n e. (ZZ>` M) -> (((K e. ZZ /\ A.j e. (M...n)A e. CC) -> sum_j e. (M...n)A = sum_k e. ((K - n)...(K - M))[_(K - k) / j]_A) -> ((K e. ZZ /\ A.j e. (M...(n + 1))A e. CC) -> sum_j e. (M...n)A = sum_k e. ((K - n)...(K - M))[_(K - k) / j]_A)))
42		nncant 5441	. . . . . . . . . . . . . 14 |- ((K e. CC /\ (n + 1) e. CC) -> (K - (K - (n + 1))) = (n + 1))
43		zcnt 6087	. . . . . . . . . . . . . . 15 |- (n e. ZZ -> n e. CC)
44		peano2cn 5316	. . . . . . . . . . . . . . 15 |- (n e. CC -> (n + 1) e. CC)
45	35, 43, 44	3syl 20	. . . . . . . . . . . . . 14 |- (n e. (ZZ>` M) -> (n + 1) e. CC)
46	42, 2, 45	syl2an 454	. . . . . . . . . . . . 13 |- ((K e. ZZ /\ n e. (ZZ>` M)) -> (K - (K - (n + 1))) = (n + 1))
47	46	csbeq1d 1994	. . . . . . . . . . . 12 |- ((K e. ZZ /\ n e. (ZZ>` M)) -> [_(K - (K - (n + 1))) / j]_A = [_(n + 1) / j]_A)
48		oprex 3968	. . . . . . . . . . . . 13 |- (K - (n + 1)) e. V
49		opreq2 3954	. . . . . . . . . . . . . 14 |- (k = (K - (n + 1)) -> (K - k) = (K - (K - (n + 1))))
50	49	csbco3g 2030	. . . . . . . . . . . . 13 |- (((K - (n + 1)) e. V /\ A.k(K - k) e. V) -> [_(K - (n