Theorem dfisum 7223

Description: Series sum with an infinite index set (i.e. an infinite series).

Assertion

Ref	Expression
dfisum	|- (M e. ZZ -> sum_k e. (ZZ>` M)A = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x})

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

Proof of Theorem dfisum

Step	Hyp	Ref	Expression
1		fzneuz 6486	. . . . . . . . . . 11 |- ((n e. (ZZ>` m) /\ M e. ZZ) -> -. (m...n) = (ZZ>` M))
2		eqcom 1484	. . . . . . . . . . . 12 |- ((m...n) = (ZZ>` M) <-> (ZZ>` M) = (m...n))
3	2	notbii 187	. . . . . . . . . . 11 |- (-. (m...n) = (ZZ>` M) <-> -. (ZZ>` M) = (m...n))
4	1, 3	sylib 198	. . . . . . . . . 10 |- ((n e. (ZZ>` m) /\ M e. ZZ) -> -. (ZZ>` M) = (m...n))
5	4	ancoms 439	. . . . . . . . 9 |- ((M e. ZZ /\ n e. (ZZ>` m)) -> -. (ZZ>` M) = (m...n))
6	5	intnanrd 698	. . . . . . . 8 |- ((M e. ZZ /\ n e. (ZZ>` m)) -> -. ((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
7	6	nrexdv 1737	. . . . . . 7 |- (M e. ZZ -> -. E.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
8	7	nexdv 1330	. . . . . 6 |- (M e. ZZ -> -. E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
9	8	nexdv 1330	. . . . 5 |- (M e. ZZ -> -. E.xE.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
10		abn0 2302	. . . . . 6 |- ({x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} =/= (/) <-> E.xE.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)))
11	10	necon1bbii 1624	. . . . 5 |- (-. E.xE.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n)) <-> {x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} = (/))
12	9, 11	sylib 198	. . . 4 |- (M e. ZZ -> {x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} = (/))
13		uz11 6400	. . . . . . . . . 10 |- (M e. ZZ -> ((ZZ>` M) = (ZZ>` m) <-> M = m))
14		eqcom 1484	. . . . . . . . . 10 |- (M = m <-> m = M)
15	13, 14	syl6bb 539	. . . . . . . . 9 |- (M e. ZZ -> ((ZZ>` M) = (ZZ>` m) <-> m = M))
16	15	anbi1d 620	. . . . . . . 8 |- (M e. ZZ -> (((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x) <-> (m = M /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)))
17	16	rexbidv 1671	. . . . . . 7 |- (M e. ZZ -> (E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x) <-> E.m e. ZZ (m = M /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)))
18		opeq1 2501	. . . . . . . . . 10 |- (m = M -> <.m, + >. = <.M, + >.)
19	18	opreq1d 3991	. . . . . . . . 9 |- (m = M -> (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) = (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)))
20	19	breq1d 2644	. . . . . . . 8 |- (m = M -> ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x <-> (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x))
21	20	ceqsrexv 1896	. . . . . . 7 |- (M e. ZZ -> (E.m e. ZZ (m = M /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x) <-> (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x))
22	17, 21	bitrd 531	. . . . . 6 |- (M e. ZZ -> (E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x) <-> (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x))
23	22	abbidv 1584	. . . . 5 |- (M e. ZZ -> {x | E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)} = {x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x})
24	23	unieqd 2526	. . . 4 |- (M e. ZZ -> U.{x | E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)} = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x})
25	12, 24	uneq12d 2196	. . 3 |- (M e. ZZ -> ({x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} u. U.{x | E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)}) = ((/) u. U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x}))
26		uncom 2187	. . . 4 |- ((/) u. U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x}) = (U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x} u. (/))
27		un0 2309	. . . 4 |- (U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x} u. (/)) = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x}
28	26, 27	eqtri 1502	. . 3 |- ((/) u. U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x}) = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x}
29	25, 28	syl6eq 1530	. 2 |- (M e. ZZ -> ({x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} u. U.{x | E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)}) = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x})
30		df-sum 7012	. 2 |- sum_k e. (ZZ>` M)A = ({x | E.mE.n e. (ZZ>` m)((ZZ>` M) = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = A} |` ZZ))` n))} u. U.{x | E.m e. ZZ ((ZZ>` M) = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x)})
31	29, 30	syl5eq 1526	1 |- (M e. ZZ -> sum_k e. (ZZ>` M)A = U.{x | (<.M, + >. seq ({<.k, y>. | y = A} |` ZZ)) ~~> x})

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   = wceq 960   e. wcel