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

Definition df-sum 12435
 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 12466. Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12614). (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jul-2013.)
Assertion
Ref Expression
df-sum
Distinct variable groups:   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-sum
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3csu 12434 . 2
5 vm . . . . . . . . 9
65cv 1648 . . . . . . . 8
7 cuz 10444 . . . . . . . 8
86, 7cfv 5413 . . . . . . 7
91, 8wss 3280 . . . . . 6
10 caddc 8949 . . . . . . . 8
11 cz 10238 . . . . . . . . 9
123cv 1648 . . . . . . . . . . 11
1312, 1wcel 1721 . . . . . . . . . 10
14 cc0 8946 . . . . . . . . . 10
1513, 2, 14cif 3699 . . . . . . . . 9
163, 11, 15cmpt 4226 . . . . . . . 8
1710, 16, 6cseq 11278 . . . . . . 7
18 vx . . . . . . . 8
1918cv 1648 . . . . . . 7
20 cli 12233 . . . . . . 7
2117, 19, 20wbr 4172 . . . . . 6
229, 21wa 359 . . . . 5
2322, 5, 11wrex 2667 . . . 4
24 c1 8947 . . . . . . . . 9
25 cfz 10999 . . . . . . . . 9
2624, 6, 25co 6040 . . . . . . . 8
27 vf . . . . . . . . 9
2827cv 1648 . . . . . . . 8
2926, 1, 28wf1o 5412 . . . . . . 7
30 vn . . . . . . . . . . 11
31 cn 9956 . . . . . . . . . . 11
3230cv 1648 . . . . . . . . . . . . 13
3332, 28cfv 5413 . . . . . . . . . . . 12
343, 33, 2csb 3211 . . . . . . . . . . 11
3530, 31, 34cmpt 4226 . . . . . . . . . 10
3610, 35, 24cseq 11278 . . . . . . . . 9
376, 36cfv 5413 . . . . . . . 8
3819, 37wceq 1649 . . . . . . 7
3929, 38wa 359 . . . . . 6
4039, 27wex 1547 . . . . 5
4140, 5, 31wrex 2667 . . . 4
4223, 41wo 358 . . 3
4342, 18cio 5375 . 2
444, 43wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  sumex  12436  sumeq1f  12437  nfsum1  12439  nfsum  12440  sumeq2w  12441  sumeq2ii  12442  cbvsum  12444  zsum  12467  fsum  12469
 Copyright terms: Public domain W3C validator