Theorem fsumcom 6917

Description: Interchange order of summation. Warning: The HTML proof page is 0.6MB in size.

Assertion

Ref	Expression
fsumcom	|- ((K e. (ZZ>` J) /\ N e. (ZZ>` M) /\ A.j e. (J...K)A.m e. (M...N)A e. CC) -> sum_j e. (J...K)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...K)A)

Distinct variable groups:   j,m,J   j,K,m   j,M,m   j,N,m

Proof of Theorem fsumcom

Step	Hyp	Ref	Expression
1		opreq2 3908	. . . . . 6 |- (k = J -> (J...k) = (J...J))
2	1	raleq1d 1765	. . . . 5 |- (k = J -> (A.j e. (J...k)A.m e. (M...N)A e. CC <-> A.j e. (J...J)A.m e. (M...N)A e. CC))
3	2	anbi2d 614	. . . 4 |- (k = J -> ((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) <-> (N e. (ZZ>` M) /\ A.j e. (J...J)A.m e. (M...N)A e. CC)))
4	1	sumeq1d 6879	. . . . 5 |- (k = J -> sum_j e. (J...k)sum_m e. (M...N)A = sum_j e. (J...J)sum_m e. (M...N)A)
5	1	sumeq1d 6879	. . . . . 6 |- (k = J -> sum_j e. (J...k)A = sum_j e. (J...J)A)
6	5	sumeq2sdv 6882	. . . . 5 |- (k = J -> sum_m e. (M...N)sum_j e. (J...k)A = sum_m e. (M...N)sum_j e. (J...J)A)
7	4, 6	eqeq12d 1465	. . . 4 |- (k = J -> (sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A <-> sum_j e. (J...J)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...J)A))
8	3, 7	imbi12d 624	. . 3 |- (k = J -> (((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) -> sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A) <-> ((N e. (ZZ>` M) /\ A.j e. (J...J)A.m e. (M...N)A e. CC) -> sum_j e. (J...J)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...J)A)))
9		opreq2 3908	. . . . . 6 |- (k = n -> (J...k) = (J...n))
10	9	raleq1d 1765	. . . . 5 |- (k = n -> (A.j e. (J...k)A.m e. (M...N)A e. CC <-> A.j e. (J...n)A.m e. (M...N)A e. CC))
11	10	anbi2d 614	. . . 4 |- (k = n -> ((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) <-> (N e. (ZZ>` M) /\ A.j e. (J...n)A.m e. (M...N)A e. CC)))
12	9	sumeq1d 6879	. . . . 5 |- (k = n -> sum_j e. (J...k)sum_m e. (M...N)A = sum_j e. (J...n)sum_m e. (M...N)A)
13	9	sumeq1d 6879	. . . . . 6 |- (k = n -> sum_j e. (J...k)A = sum_j e. (J...n)A)
14	13	sumeq2sdv 6882	. . . . 5 |- (k = n -> sum_m e. (M...N)sum_j e. (J...k)A = sum_m e. (M...N)sum_j e. (J...n)A)
15	12, 14	eqeq12d 1465	. . . 4 |- (k = n -> (sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A <-> sum_j e. (J...n)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...n)A))
16	11, 15	imbi12d 624	. . 3 |- (k = n -> (((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) -> sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A) <-> ((N e. (ZZ>` M) /\ A.j e. (J...n)A.m e. (M...N)A e. CC) -> sum_j e. (J...n)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...n)A)))
17		opreq2 3908	. . . . . 6 |- (k = (n + 1) -> (J...k) = (J...(n + 1)))
18	17	raleq1d 1765	. . . . 5 |- (k = (n + 1) -> (A.j e. (J...k)A.m e. (M...N)A e. CC <-> A.j e. (J...(n + 1))A.m e. (M...N)A e. CC))
19	18	anbi2d 614	. . . 4 |- (k = (n + 1) -> ((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) <-> (N e. (ZZ>` M) /\ A.j e. (J...(n + 1))A.m e. (M...N)A e. CC)))
20	17	sumeq1d 6879	. . . . 5 |- (k = (n + 1) -> sum_j e. (J...k)sum_m e. (M...N)A = sum_j e. (J...(n + 1))sum_m e. (M...N)A)
21	17	sumeq1d 6879	. . . . . 6 |- (k = (n + 1) -> sum_j e. (J...k)A = sum_j e. (J...(n + 1))A)
22	21	sumeq2sdv 6882	. . . . 5 |- (k = (n + 1) -> sum_m e. (M...N)sum_j e. (J...k)A = sum_m e. (M...N)sum_j e. (J...(n + 1))A)
23	20, 22	eqeq12d 1465	. . . 4 |- (k = (n + 1) -> (sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A <-> sum_j e. (J...(n + 1))sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...(n + 1))A))
24	19, 23	imbi12d 624	. . 3 |- (k = (n + 1) -> (((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) -> sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A) <-> ((N e. (ZZ>` M) /\ A.j e. (J...(n + 1))A.m e. (M...N)A e. CC) -> sum_j e. (J...(n + 1))sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...(n + 1))A)))
25		opreq2 3908	. . . . . 6 |- (k = K -> (J...k) = (J...K))
26	25	raleq1d 1765	. . . . 5 |- (k = K -> (A.j e. (J...k)A.m e. (M...N)A e. CC <-> A.j e. (J...K)A.m e. (M...N)A e. CC))
27	26	anbi2d 614	. . . 4 |- (k = K -> ((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) <-> (N e. (ZZ>` M) /\ A.j e. (J...K)A.m e. (M...N)A e. CC)))
28	25	sumeq1d 6879	. . . . 5 |- (k = K -> sum_j e. (J...k)sum_m e. (M...N)A = sum_j e. (J...K)sum_m e. (M...N)A)
29	25	sumeq1d 6879	. . . . . 6 |- (k = K -> sum_j e. (J...k)A = sum_j e. (J...K)A)
30	29	sumeq2sdv 6882	. . . . 5 |- (k = K -> sum_m e. (M...N)sum_j e. (J...k)A = sum_m e. (M...N)sum_j e. (J...K)A)
31	28, 30	eqeq12d 1465	. . . 4 |- (k = K -> (sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A <-> sum_j e. (J...K)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...K)A))
32	27, 31	imbi12d 624	. . 3 |- (k = K -> (((N e. (ZZ>` M) /\ A.j e. (J...k)A.m e. (M...N)A e. CC) -> sum_j e. (J...k)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...k)A) <-> ((N e. (ZZ>` M) /\ A.j e. (J...K)A.m e. (M...N)A e. CC) -> sum_j e. (J...K)sum_m e. (M...N)A = sum_m e. (M...N)sum_j e. (J...K)A)))
33		csbfsum 6916	. . . . . 6 |- ((J e. ZZ /\ N e. (ZZ>` M) /\ A.m e. (M...N)[_J / j]_A e. CC) -> [_J / j]_sum_m e. (M...N)A = sum_m e. (M...N)[_J / j]_A)
34		pm3.26 319	. . . . . 6 |- ((J e. ZZ /\ (N e. (ZZ>` M) /\ A.j e. (J...J)