Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sumdc Unicode version

Definition df-sumdc 11154
 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. In both cases we have an expression so that we only need to be defined where . In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e. finite sets of integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11322). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.)
Assertion
Ref Expression
df-sumdc DECID
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-sumdc
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3csu 11153 . 2
5 vm . . . . . . . . 9
65cv 1331 . . . . . . . 8
7 cuz 9349 . . . . . . . 8
86, 7cfv 5130 . . . . . . 7
91, 8wss 3075 . . . . . 6
10 vj . . . . . . . . . 10
1110cv 1331 . . . . . . . . 9
1211, 1wcel 1481 . . . . . . . 8
1312wdc 820 . . . . . . 7 DECID
1413, 10, 8wral 2417 . . . . . 6 DECID
15 caddc 7646 . . . . . . . 8
16 vn . . . . . . . . 9
17 cz 9077 . . . . . . . . 9
1816cv 1331 . . . . . . . . . . 11
1918, 1wcel 1481 . . . . . . . . . 10
203, 18, 2csb 3006 . . . . . . . . . 10
21 cc0 7643 . . . . . . . . . 10
2219, 20, 21cif 3478 . . . . . . . . 9
2316, 17, 22cmpt 3996 . . . . . . . 8
2415, 23, 6cseq 10248 . . . . . . 7
25 vx . . . . . . . 8
2625cv 1331 . . . . . . 7
27 cli 11078 . . . . . . 7
2824, 26, 27wbr 3936 . . . . . 6
299, 14, 28w3a 963 . . . . 5 DECID
3029, 5, 17wrex 2418 . . . 4 DECID
31 c1 7644 . . . . . . . . 9
32 cfz 9820 . . . . . . . . 9
3331, 6, 32co 5781 . . . . . . . 8
34 vf . . . . . . . . 9
3534cv 1331 . . . . . . . 8
3633, 1, 35wf1o 5129 . . . . . . 7
37 cn 8743 . . . . . . . . . . 11
38 cle 7824 . . . . . . . . . . . . 13
3918, 6, 38wbr 3936 . . . . . . . . . . . 12
4018, 35cfv 5130 . . . . . . . . . . . . 13
413, 40, 2csb 3006 . . . . . . . . . . . 12
4239, 41, 21cif 3478 . . . . . . . . . . 11
4316, 37, 42cmpt 3996 . . . . . . . . . 10
4415, 43, 31cseq 10248 . . . . . . . . 9
456, 44cfv 5130 . . . . . . . 8
4626, 45wceq 1332 . . . . . . 7
4736, 46wa 103 . . . . . 6
4847, 34wex 1469 . . . . 5
4948, 5, 37wrex 2418 . . . 4
5030, 49wo 698 . . 3 DECID
5150, 25cio 5093 . 2 DECID
524, 51wceq 1332 1 DECID
 Colors of variables: wff set class This definition is referenced by:  sumeq1  11155  nfsum1  11156  nfsum  11157  sumeq2  11159  cbvsum  11160  zsumdc  11184  fsum3  11187
 Copyright terms: Public domain W3C validator