Definition df-sum 10191

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). 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. (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 ) ) , CC ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` 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 10190	. 2 class sum_ k e. A B
5		vm	. . . . . . . . 9 setvar m
6	5	cv 1283	. . . . . . . 8 class m
7		cuz 8619	. . . . . . . 8 class ZZ>=
8	6, 7	cfv 4922	. . . . . . 7 class ( ZZ>= ` m )
9	1, 8	wss 2973	. . . . . 6 wff A C_ ( ZZ>= ` m )
10		caddc 6984	. . . . . . . 8 class +
11		cc 6979	. . . . . . . 8 class CC
12		vn	. . . . . . . . 9 setvar n
13		cz 8351	. . . . . . . . 9 class ZZ
14	12	cv 1283	. . . . . . . . . . 11 class n
15	14, 1	wcel 1433	. . . . . . . . . 10 wff n e. A
16	3, 14, 2	csb 2908	. . . . . . . . . 10 class [_ n / k ]_ B
17		cc0 6981	. . . . . . . . . 10 class 0
18	15, 16, 17	cif 3351	. . . . . . . . 9 class if ( n e. A , [_ n / k ]_ B , 0 )
19	12, 13, 18	cmpt 3839	. . . . . . . 8 class ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
20	10, 11, 19, 6	cseq 9431	. . . . . . 7 class seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC )
21		vx	. . . . . . . 8 setvar x
22	21	cv 1283	. . . . . . 7 class x
23		cli 10117	. . . . . . 7 class ~~>
24	20, 22, 23	wbr 3785	. . . . . 6 wff seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC ) ~~> x
25	9, 24	wa 102	. . . . 5 wff ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC ) ~~> x )
26	25, 5, 13	wrex 2349	. . . 4 wff E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC ) ~~> x )
27		c1 6982	. . . . . . . . 9 class 1
28		cfz 9029	. . . . . . . . 9 class ...
29	27, 6, 28	co 5532	. . . . . . . 8 class ( 1 ... m )
30		vf	. . . . . . . . 9 setvar f
31	30	cv 1283	. . . . . . . 8 class f
32	29, 1, 31	wf1o 4921	. . . . . . 7 wff f : ( 1 ... m ) -1-1-onto-> A
33		cn 8039	. . . . . . . . . . 11 class NN
34	14, 31	cfv 4922	. . . . . . . . . . . 12 class ( f ` n )
35	3, 34, 2	csb 2908	. . . . . . . . . . 11 class [_ ( f ` n ) / k ]_ B
36	12, 33, 35	cmpt 3839	. . . . . . . . . 10 class ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
37	10, 11, 36, 27	cseq 9431	. . . . . . . . 9 class seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC )
38	6, 37	cfv 4922	. . . . . . . 8 class ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m )
39	22, 38	wceq 1284	. . . . . . 7 wff x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m )
40	32, 39	wa 102	. . . . . 6 wff ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) )
41	40, 30	wex 1421	. . . . 5 wff E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) )
42	41, 5, 33	wrex 2349	. . . 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 ) , CC ) ` m ) )
43	26, 42	wo 661	. . 3 wff ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) , CC ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) ) )
44	43, 21	cio 4885	. 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 ) ) , CC ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) ) ) )
45	4, 44	wceq 1284	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 ) ) , CC ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) , CC ) ` m ) ) ) )

This definition is referenced by:  sumeq1  10192  nfsum1  10193  nfsum  10194