Definition df-sum 6980

Description: Define the sum of a series with an index set of integers A. k is normally a free variable in B, i.e. B can be thought of as B(k). The definition is meaningful when A is a finite set of sequential integers (representing a finite sum over them) or a set of upper integers (representing an infinite sum, when the sum converges). The left-hand side of the union expresses the finite sum case, and the right-hand side expresses the infinite sum case. In either case, the other side of the union equals the empty set. Examples: sum_k e. (2...4) k means 2 + 3 + 4 = 9, and sum_k e. NN (1 / (2^k)) means 1/2 + 1/4 + 1/8 + ... = 1. Note: The restrictions to ZZ force the class abstractions to be sets.

Assertion

Ref	Expression
df-sum	|- sum_k e. A B = ({x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)})

Distinct variable groups:   k,m,n,x,y   A,m,n,x,y   B,m,n,x,y

Detailed syntax breakdown of Definition df-sum

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 set k
4	1, 2, 3	csu 6979	. 2 class sum_k e. A B
5		vm	. . . . . . . . . 10 set m
6	5	cv 957	. . . . . . . . 9 class m
7		vn	. . . . . . . . . 10 set n
8	7	cv 957	. . . . . . . . 9 class n
9		cfz 6468	. . . . . . . . 9 class ...
10	6, 8, 9	co 3969	. . . . . . . 8 class (m...n)
11	1, 10	wceq 958	. . . . . . 7 wff A = (m...n)
12		vx	. . . . . . . . 9 set x
13	12	cv 957	. . . . . . . 8 class x
14		caddc 5249	. . . . . . . . . . 11 class +
15	6, 14	cop 2415	. . . . . . . . . 10 class <.m, + >.
16		vy	. . . . . . . . . . . . . 14 set y
17	16	cv 957	. . . . . . . . . . . . 13 class y
18	17, 2	wceq 958	. . . . . . . . . . . 12 wff y = B
19	18, 3, 16	copab 2671	. . . . . . . . . . 11 class {<.k, y>. | y = B}
20		cz 5310	. . . . . . . . . . 11 class ZZ
21	19, 20	cres 3178	. . . . . . . . . 10 class ({<.k, y>. | y = B} |` ZZ)
22		cseqz 6532	. . . . . . . . . 10 class seq
23	15, 21, 22	co 3969	. . . . . . . . 9 class (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))
24	8, 23	cfv 3188	. . . . . . . 8 class ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n)
25	13, 24	wcel 960	. . . . . . 7 wff x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n)
26	11, 25	wa 223	. . . . . 6 wff (A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))
27		cuz 6418	. . . . . . 7 class ZZ>
28	6, 27	cfv 3188	. . . . . 6 class (ZZ>` m)
29	26, 7, 28	wrex 1649	. . . . 5 wff E.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))
30	29, 5	wex 982	. . . 4 wff E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))
31	30, 12	cab 1466	. . 3 class {x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))}
32	1, 28	wceq 958	. . . . . . 7 wff A = (ZZ>` m)
33		cli 6974	. . . . . . . 8 class ~~>
34	23, 13, 33	wbr 2624	. . . . . . 7 wff (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x
35	32, 34	wa 223	. . . . . 6 wff (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)
36	35, 5, 20	wrex 1649	. . . . 5 wff E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)
37	36, 12	cab 1466	. . . 4 class {x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)}
38	37	cuni 2507	. . 3 class U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)}
39	31, 38	cun 2048	. 2 class ({x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)})
40	4, 39	wceq 958	1 wff sum_k e. A B = ({x | E.mE.n e. (ZZ>` m)(A = (m...n) /\ x e. ((<.m, + >. seq ({<.k, y>. | y = B} |` ZZ))` n))} u. U.{x | E.m e. ZZ (A = (ZZ>` m) /\ (<.m, + >. seq ({<.k, y>. | y = B} |` ZZ)) ~~> x)})

This definition is referenced by:  sumex 6981  sumeq1 6982  hbsum1 6983  hbsum 6984  sumeq2 6985  cbvsum 6986  dffsum 6998  dfisum 7191

Copyright terms: Public domain