MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sum Unicode version

Definition df-sum 13509
Description: Define the sum of a series with an index set of integers . is normally a free variable in , i.e. can be thought of as ( ). 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 13539. Examples: sum_ e.{1,2,4} means 1 2 4=7, and sum_ e. means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 13691). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)
Assertion
Ref Expression
df-sum
Distinct variable groups:   , , , ,   , , , ,   , , , ,

Detailed syntax breakdown of Definition df-sum
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3csu 13508 . 2
5 vm . . . . . . . . 9
65cv 1394 . . . . . . . 8
7 cuz 11110 . . . . . . . 8
86, 7cfv 5593 . . . . . . 7
91, 8wss 3475 . . . . . 6
10 caddc 9516 . . . . . . . 8
11 vn . . . . . . . . 9
12 cz 10889 . . . . . . . . 9
1311cv 1394 . . . . . . . . . . 11
1413, 1wcel 1818 . . . . . . . . . 10
153, 13, 2csb 3434 . . . . . . . . . 10
16 cc0 9513 . . . . . . . . . 10
1714, 15, 16cif 3941 . . . . . . . . 9
1811, 12, 17cmpt 4510 . . . . . . . 8
1910, 18, 6cseq 12107 . . . . . . 7
20 vx . . . . . . . 8
2120cv 1394 . . . . . . 7
22 cli 13307 . . . . . . 7
2319, 21, 22wbr 4452 . . . . . 6
249, 23wa 369 . . . . 5
2524, 5, 12wrex 2808 . . . 4
26 c1 9514 . . . . . . . . 9
27 cfz 11701 . . . . . . . . 9
2826, 6, 27co 6296 . . . . . . . 8
29 vf . . . . . . . . 9
3029cv 1394 . . . . . . . 8
3128, 1, 30wf1o 5592 . . . . . . 7
32 cn 10561 . . . . . . . . . . 11
3313, 30cfv 5593 . . . . . . . . . . . 12
343, 33, 2csb 3434 . . . . . . . . . . 11
3511, 32, 34cmpt 4510 . . . . . . . . . 10
3610, 35, 26cseq 12107 . . . . . . . . 9
376, 36cfv 5593 . . . . . . . 8
3821, 37wceq 1395 . . . . . . 7
3931, 38wa 369 . . . . . 6
4039, 29wex 1612 . . . . 5
4140, 5, 32wrex 2808 . . . 4
4225, 41wo 368 . . 3
4342, 20cio 5554 . 2
444, 43wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  sumex  13510  sumeq1  13511  nfsum1  13512  nfsum  13513  sumeq2w  13514  sumeq2ii  13515  cbvsum  13517  zsum  13540  fsum  13542
  Copyright terms: Public domain W3C validator