Definition df-sum 14417

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 ). This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers) by summo 14448. Examples: sum_ k e. { 1 , 2 , 4 } k means 1 + 2 + 4 = 7, and sum_ k e. NN ( 1 / ( 2 ^ k ) ) = 1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 14614). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Assertion

Ref	Expression
df-sum	|- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )

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

Allowed substitution hints:   A( k)   B( k)

Detailed syntax breakdown of Definition df-sum

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 setvar k
4	1, 2, 3	csu 14416	. 2 class sum_ k e. A B
5		vm	. . . . . . . . 9 setvar m
6	5	cv 1482	. . . . . . . 8 class m
7		cuz 11687	. . . . . . . 8 class ZZ>=
8	6, 7	cfv 5888	. . . . . . 7 class ( ZZ>= ` m )
9	1, 8	wss 3574	. . . . . 6 wff A C_ ( ZZ>= ` m )
10		caddc 9939	. . . . . . . 8 class +
11		vn	. . . . . . . . 9 setvar n
12		cz 11377	. . . . . . . . 9 class ZZ
13	11	cv 1482	. . . . . . . . . . 11 class n
14	13, 1	wcel 1990	. . . . . . . . . 10 wff n e. A
15	3, 13, 2	csb 3533	. . . . . . . . . 10 class [_ n / k ]_ B
16		cc0 9936	. . . . . . . . . 10 class 0
17	14, 15, 16	cif 4086	. . . . . . . . 9 class if ( n e. A , [_ n / k ]_ B , 0 )
18	11, 12, 17	cmpt 4729	. . . . . . . 8 class ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
19	10, 18, 6	cseq 12801	. . . . . . 7 class seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
20		vx	. . . . . . . 8 setvar x
21	20	cv 1482	. . . . . . 7 class x
22		cli 14215	. . . . . . 7 class ~~>
23	19, 21, 22	wbr 4653	. . . . . 6 wff seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x
24	9, 23	wa 384	. . . . 5 wff ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
25	24, 5, 12	wrex 2913	. . . 4 wff E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
26		c1 9937	. . . . . . . . 9 class 1
27		cfz 12326	. . . . . . . . 9 class ...
28	26, 6, 27	co 6650	. . . . . . . 8 class ( 1 ... m )
29		vf	. . . . . . . . 9 setvar f
30	29	cv 1482	. . . . . . . 8 class f
31	28, 1, 30	wf1o 5887	. . . . . . 7 wff f : ( 1 ... m ) -1-1-onto-> A
32		cn 11020	. . . . . . . . . . 11 class NN
33	13, 30	cfv 5888	. . . . . . . . . . . 12 class ( f ` n )
34	3, 33, 2	csb 3533	. . . . . . . . . . 11 class [_ ( f ` n ) / k ]_ B
35	11, 32, 34	cmpt 4729	. . . . . . . . . 10 class ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
36	10, 35, 26	cseq 12801	. . . . . . . . 9 class seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
37	6, 36	cfv 5888	. . . . . . . 8 class ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
38	21, 37	wceq 1483	. . . . . . 7 wff x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
39	31, 38	wa 384	. . . . . 6 wff ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
40	39, 29	wex 1704	. . . . 5 wff E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
41	40, 5, 32	wrex 2913	. . . 4 wff E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
42	25, 41	wo 383	. . 3 wff ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
43	42, 20	cio 5849	. 2 class ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
44	4, 43	wceq 1483	1 wff sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )

This definition is referenced by:  sumex  14418  sumeq1  14419  nfsum1  14420  nfsum  14421  sumeq2w  14422  sumeq2ii  14423  cbvsum  14425  zsum  14449  fsum  14451