# Metamath Proof Explorer

## Definition df-sum

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 sets of integers) by summo . 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 ). (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Assertion df-sum

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vk ${setvar}{k}$
1 cA ${class}{A}$
2 cB ${class}{B}$
3 1 2 0 csu ${class}\sum _{{k}\in {A}}{B}$
4 vx ${setvar}{x}$
5 vm ${setvar}{m}$
6 cz ${class}ℤ$
7 cuz ${class}{ℤ}_{\ge }$
8 5 cv ${setvar}{m}$
9 8 7 cfv ${class}{ℤ}_{\ge {m}}$
10 1 9 wss ${wff}{A}\subseteq {ℤ}_{\ge {m}}$
11 caddc ${class}+$
12 vn ${setvar}{n}$
13 12 cv ${setvar}{n}$
14 13 1 wcel ${wff}{n}\in {A}$
15 0 13 2 csb
16 cc0 ${class}0$
17 14 15 16 cif
18 12 6 17 cmpt
19 11 18 8 cseq
20 cli ${class}⇝$
21 4 cv ${setvar}{x}$
22 19 21 20 wbr
23 10 22 wa
24 23 5 6 wrex
25 cn ${class}ℕ$
26 vf ${setvar}{f}$
27 26 cv ${setvar}{f}$
28 c1 ${class}1$
29 cfz ${class}\dots$
30 28 8 29 co ${class}\left(1\dots {m}\right)$
31 30 1 27 wf1o ${wff}{f}:\left(1\dots {m}\right)\underset{1-1 onto}{⟶}{A}$
32 13 27 cfv ${class}{f}\left({n}\right)$
33 0 32 2 csb
34 12 25 33 cmpt
35 11 34 28 cseq
36 8 35 cfv
37 21 36 wceq
38 31 37 wa
39 38 26 wex
40 39 5 25 wrex
41 24 40 wo
42 41 4 cio
43 3 42 wceq