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

Definition df-isum 10743
 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. (Contributed by Jim Kingdon, 15-Feb-2022.)
Assertion
Ref Expression
df-isum DECID
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   ()

Detailed syntax breakdown of Definition df-isum
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 vk . . 3
41, 2, 3csu 10742 . 2
5 vm . . . . . . . . 9
65cv 1288 . . . . . . . 8
7 cuz 9019 . . . . . . . 8
86, 7cfv 5015 . . . . . . 7
91, 8wss 2999 . . . . . 6
10 vj . . . . . . . . . 10
1110cv 1288 . . . . . . . . 9
1211, 1wcel 1438 . . . . . . . 8
1312wdc 780 . . . . . . 7 DECID
1413, 10, 8wral 2359 . . . . . 6 DECID
15 caddc 7353 . . . . . . . 8
16 cc 7348 . . . . . . . 8
17 vn . . . . . . . . 9
18 cz 8750 . . . . . . . . 9
1917cv 1288 . . . . . . . . . . 11
2019, 1wcel 1438 . . . . . . . . . 10
213, 19, 2csb 2933 . . . . . . . . . 10
22 cc0 7350 . . . . . . . . . 10
2320, 21, 22cif 3393 . . . . . . . . 9
2417, 18, 23cmpt 3899 . . . . . . . 8
2515, 16, 24, 6cseq4 9851 . . . . . . 7
26 vx . . . . . . . 8
2726cv 1288 . . . . . . 7
28 cli 10666 . . . . . . 7
2925, 27, 28wbr 3845 . . . . . 6
309, 14, 29w3a 924 . . . . 5 DECID
3130, 5, 18wrex 2360 . . . 4 DECID
32 c1 7351 . . . . . . . . 9
33 cfz 9424 . . . . . . . . 9
3432, 6, 33co 5652 . . . . . . . 8
35 vf . . . . . . . . 9
3635cv 1288 . . . . . . . 8
3734, 1, 36wf1o 5014 . . . . . . 7
38 cn 8422 . . . . . . . . . . 11
39 cle 7523 . . . . . . . . . . . . 13
4019, 6, 39wbr 3845 . . . . . . . . . . . 12
4119, 36cfv 5015 . . . . . . . . . . . . 13
423, 41, 2csb 2933 . . . . . . . . . . . 12
4340, 42, 22cif 3393 . . . . . . . . . . 11
4417, 38, 43cmpt 3899 . . . . . . . . . 10
4515, 16, 44, 32cseq4 9851 . . . . . . . . 9
466, 45cfv 5015 . . . . . . . 8
4727, 46wceq 1289 . . . . . . 7
4837, 47wa 102 . . . . . 6
4948, 35wex 1426 . . . . 5
5049, 5, 38wrex 2360 . . . 4
5131, 50wo 664 . . 3 DECID
5251, 26cio 4978 . 2 DECID
534, 52wceq 1289 1 DECID
 Colors of variables: wff set class This definition is referenced by:  sumeq1  10744  nfsum1  10745  nfsum  10746  sumeq2  10748  cbvsum  10749  zisum  10774  fisum  10778
 Copyright terms: Public domain W3C validator