Metamath Proof Explorer

Definition df-sum

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. 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 ⊢∑k∈AB=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m

Detailed syntax breakdown

Step Hyp Ref Expression
0 vk setvark
1 cA classA
2 cB classB
3 1 2 0 csu class∑k∈AB
4 vx setvarx
5 vm setvarm
6 cz classℤ
7 cuz classℤ≥
8 5 cv setvarm
9 8 7 cfv classℤ≥m
10 1 9 wss wffA⊆ℤ≥m
11 caddc class+
12 vn setvarn
13 12 cv setvarn
14 13 1 wcel wffn∈A
15 0 13 2 csb class⦋n/k⦌B
16 cc0 class0
17 14 15 16 cif classifn∈A⦋n/k⦌B0
18 12 6 17 cmpt classn∈ℤ⟼ifn∈A⦋n/k⦌B0
19 11 18 8 cseq classseqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0
20 cli class⇝
21 4 cv setvarx
22 19 21 20 wbr wffseqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
23 10 22 wa wffA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
24 23 5 6 wrex wff∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x
25 cn classℕ
26 vf setvarf
27 26 cv setvarf
28 c1 class1
29 cfz class…
30 28 8 29 co class1…m
31 30 1 27 wf1o wfff:1…m⟶1-1 ontoA
32 13 27 cfv classf⁡n
33 0 32 2 csb class⦋f⁡n/k⦌B
34 12 25 33 cmpt classn∈ℕ⟼⦋f⁡n/k⦌B
35 11 34 28 cseq classseq1+n∈ℕ⟼⦋f⁡n/k⦌B
36 8 35 cfv classseq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
37 21 36 wceq wffx=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
38 31 37 wa wfff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
39 38 26 wex wff∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
40 39 5 25 wrex wff∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
41 24 40 wo wff∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
42 41 4 cio classιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m
43 3 42 wceq wff∑k∈AB=ιx|∃m∈ℤA⊆ℤ≥m∧seqm+n∈ℤ⟼ifn∈A⦋n/k⦌B0⇝x∨∃m∈ℕ∃ff:1…m⟶1-1 ontoA∧x=seq1+n∈ℕ⟼⦋f⁡n/k⦌B⁡m