Theorem dffsum 7005

Description: Special case of series sum over a finite index set.

Assertion

Ref	Expression
dffsum	|- (N e. (ZZ>` M) -> sum_k e. (M...N)A = ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))

Distinct variable groups:   y,A   y,M   y,N   y,k

Proof of Theorem dffsum

Step	Hyp	Ref	Expression
1		visset 1816	. . . . . . . . . . 11 |- n e. V
2		fzoptht 6510	. . . . . . . . . . 11 |- ((N e. (ZZ>` M) /\ n e. V) -> ((M...N) = (m...n) <-> (M = m /\ N = n)))
3	1, 2	mpan2 698	. . . . . . . . . 10 |- (N e. (ZZ>` M) -> ((M...N) = (m...n) <-> (M = m /\ N = n)))
4		eqcom 1480	. . . . . . . . . . 11 |- (M = m <-> m = M)
5		eqcom 1480	. . . . . . . . . . 11 |- (N = n <-> n = N)
6	4, 5	anbi12i 484	. . . . . . . . . 10 |- ((M = m /\ N = n) <-> (m = M /\ n = N))
7	3, 6	syl6bb 538	. . . . . . . . 9 |- (N e. (ZZ>` M) -> ((M...N) = (m...n) <-> (m = M /\ n = N)))
8	7	anbi1d 619	. . . . . . . 8 |- (N e. (ZZ>` M) -> (((M...N) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> ((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
9	8	rexbidv 1667	. . . . . . 7 |- (N e. (ZZ>` M) -> (E.n e. (ZZ>` m)((M...N) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.n e. (ZZ>` m)((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
10	9	exbidv 1281	. . . . . 6 |- (N e. (ZZ>` M) -> (E.mE.n e. (ZZ>` m)((M...N) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.mE.n e. (ZZ>` m)((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
11		breq1 2628	. . . . . . . . . . 11 |- (m = M -> (m <_ n <-> M <_ n))
12		opeq1 2492	. . . . . . . . . . . . . 14 |- (m = M -> <.m, + >. = <.M, + >.)
13	12	opreq1d 3982	. . . . . . . . . . . . 13 |- (m = M -> (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) = (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)))
14	13	fveq1d 3733	. . . . . . . . . . . 12 |- (m = M -> ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n) = ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))
15	14	eleq2d 1544	. . . . . . . . . . 11 |- (m = M -> (x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n) <-> x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
16	11, 15	anbi12d 630	. . . . . . . . . 10 |- (m = M -> ((m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> (M <_ n /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
17		breq2 2629	. . . . . . . . . . 11 |- (n = N -> (M <_ n <-> M <_ N))
18		fveq2 3731	. . . . . . . . . . . 12 |- (n = N -> ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n) = ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))
19	18	eleq2d 1544	. . . . . . . . . . 11 |- (n = N -> (x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n) <-> x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N)))
20	17, 19	anbi12d 630	. . . . . . . . . 10 |- (n = N -> ((M <_ n /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> (M <_ N /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))))
21	16, 20	ceqsrex2v 1893	. . . . . . . . 9 |- ((M e. ZZ /\ N e. ZZ) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> (M <_ N /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))))
22		eluzel2 6432	. . . . . . . . 9 |- (N e. (ZZ>` M) -> M e. ZZ)
23		eluzelz 6431	. . . . . . . . 9 |- (N e. (ZZ>` M) -> N e. ZZ)
24	21, 22, 23	sylanc 473	. . . . . . . 8 |- (N e. (ZZ>` M) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> (M <_ N /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))))
25		eluzle 6433	. . . . . . . . 9 |- (N e. (ZZ>` M) -> M <_ N)
26	25	biantrurd 729	. . . . . . . 8 |- (N e. (ZZ>` M) -> (x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N) <-> (M <_ N /\ x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N))))
27	24, 26	bitr4d 533	. . . . . . 7 |- (N e. (ZZ>` M) -> (E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N)))
28		2rexuz 6454	. . . . . . . 8 |- (E.mE.n e. (ZZ>` m)((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.m e. ZZ E.n e. ZZ (m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
29		an12 486	. . . . . . . . 9 |- ((m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
30	29	2rexbii 1673	. . . . . . . 8 |- (E.m e. ZZ E.n e. ZZ (m <_ n /\ ((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))) <-> E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
31	28, 30	bitr 173	. . . . . . 7 |- (E.mE.n e. (ZZ>` m)((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> E.m e. ZZ E.n e. ZZ ((m = M /\ n = N) /\ (m <_ n /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))))
32	27, 31	syl5bb 534	. . . . . 6 |- (N e. (ZZ>` M) -> (E.mE.n e. (ZZ>` m)((m = M /\ n = N) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> x e. ((<.M, + >. seq ({<.k, y>. | y = A} |` ZZ))` N)))
33	10, 32	bitrd 530	. . . . 5 |- (N e. (ZZ>` M) -> (E.mE.n e. (ZZ>` m)((M...N) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> x e. ((<.M, + >. seq ({<.k, y>.