Definition df-sumdc 11905

Description: Define the sum of a series with an index set of integers A. The variable 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. In both cases we have an if expression so that we only need B to be defined where k e. A. In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers). 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 12073). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)

Assertion

Ref	Expression
df-sumdc	|- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) ) ) )

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

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

Detailed syntax breakdown of Definition df-sumdc

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 setvar k
4	1, 2, 3	csu 11904	. 2 class sum_ k e. A B
5		vm	. . . . . . . . 9 setvar m
6	5	cv 1394	. . . . . . . 8 class m
7		cuz 9745	. . . . . . . 8 class ZZ>=
8	6, 7	cfv 5324	. . . . . . 7 class ( ZZ>= ` m )
9	1, 8	wss 3198	. . . . . 6 wff A C_ ( ZZ>= ` m )
10		vj	. . . . . . . . . 10 setvar j
11	10	cv 1394	. . . . . . . . 9 class j
12	11, 1	wcel 2200	. . . . . . . 8 wff j e. A
13	12	wdc 839	. . . . . . 7 wff DECID j e. A
14	13, 10, 8	wral 2508	. . . . . 6 wff A. j e. ( ZZ>= ` m )DECID j e. A
15		caddc 8025	. . . . . . . 8 class +
16		vn	. . . . . . . . 9 setvar n
17		cz 9469	. . . . . . . . 9 class ZZ
18	16	cv 1394	. . . . . . . . . . 11 class n
19	18, 1	wcel 2200	. . . . . . . . . 10 wff n e. A
20	3, 18, 2	csb 3125	. . . . . . . . . 10 class [_ n / k ]_ B
21		cc0 8022	. . . . . . . . . 10 class 0
22	19, 20, 21	cif 3603	. . . . . . . . 9 class if ( n e. A , [_ n / k ]_ B , 0 )
23	16, 17, 22	cmpt 4148	. . . . . . . 8 class ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
24	15, 23, 6	cseq 10699	. . . . . . 7 class seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
25		vx	. . . . . . . 8 setvar x
26	25	cv 1394	. . . . . . 7 class x
27		cli 11829	. . . . . . 7 class ~~>
28	24, 26, 27	wbr 4086	. . . . . 6 wff seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x
29	9, 14, 28	w3a 1002	. . . . 5 wff ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
30	29, 5, 17	wrex 2509	. . . 4 wff E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
31		c1 8023	. . . . . . . . 9 class 1
32		cfz 10233	. . . . . . . . 9 class ...
33	31, 6, 32	co 6013	. . . . . . . 8 class ( 1 ... m )
34		vf	. . . . . . . . 9 setvar f
35	34	cv 1394	. . . . . . . 8 class f
36	33, 1, 35	wf1o 5323	. . . . . . 7 wff f : ( 1 ... m ) -1-1-onto-> A
37		cn 9133	. . . . . . . . . . 11 class NN
38		cle 8205	. . . . . . . . . . . . 13 class <_
39	18, 6, 38	wbr 4086	. . . . . . . . . . . 12 wff n <_ m
40	18, 35	cfv 5324	. . . . . . . . . . . . 13 class ( f ` n )
41	3, 40, 2	csb 3125	. . . . . . . . . . . 12 class [_ ( f ` n ) / k ]_ B
42	39, 41, 21	cif 3603	. . . . . . . . . . 11 class if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 )
43	16, 37, 42	cmpt 4148	. . . . . . . . . 10 class ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) )
44	15, 43, 31	cseq 10699	. . . . . . . . 9 class seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) )
45	6, 44	cfv 5324	. . . . . . . 8 class ( seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m )
46	26, 45	wceq 1395	. . . . . . 7 wff x = ( seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m )
47	36, 46	wa 104	. . . . . 6 wff ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) )
48	47, 34	wex 1538	. . . . 5 wff E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) )
49	48, 5, 37	wrex 2509	. . . 4 wff E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) )
50	30, 49	wo 713	. . 3 wff ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) ) )
51	50, 25	cio 5282	. 2 class ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) ) ) )
52	4, 51	wceq 1395	1 wff sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A /\ 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 |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 0 ) ) ) ` m ) ) ) )

This definition is referenced by:  sumeq1  11906  nfsum1  11907  nfsum  11908  sumeq2  11910  cbvsum  11911  zsumdc  11935  fsum3  11938