Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sumdc | Unicode version |
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 11296). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.) |
Ref | Expression |
---|---|
df-sumdc | DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | vk | . . 3 | |
4 | 1, 2, 3 | csu 11127 | . 2 |
5 | vm | . . . . . . . . 9 | |
6 | 5 | cv 1330 | . . . . . . . 8 |
7 | cuz 9331 | . . . . . . . 8 | |
8 | 6, 7 | cfv 5123 | . . . . . . 7 |
9 | 1, 8 | wss 3071 | . . . . . 6 |
10 | vj | . . . . . . . . . 10 | |
11 | 10 | cv 1330 | . . . . . . . . 9 |
12 | 11, 1 | wcel 1480 | . . . . . . . 8 |
13 | 12 | wdc 819 | . . . . . . 7 DECID |
14 | 13, 10, 8 | wral 2416 | . . . . . 6 DECID |
15 | caddc 7628 | . . . . . . . 8 | |
16 | vn | . . . . . . . . 9 | |
17 | cz 9059 | . . . . . . . . 9 | |
18 | 16 | cv 1330 | . . . . . . . . . . 11 |
19 | 18, 1 | wcel 1480 | . . . . . . . . . 10 |
20 | 3, 18, 2 | csb 3003 | . . . . . . . . . 10 |
21 | cc0 7625 | . . . . . . . . . 10 | |
22 | 19, 20, 21 | cif 3474 | . . . . . . . . 9 |
23 | 16, 17, 22 | cmpt 3989 | . . . . . . . 8 |
24 | 15, 23, 6 | cseq 10223 | . . . . . . 7 |
25 | vx | . . . . . . . 8 | |
26 | 25 | cv 1330 | . . . . . . 7 |
27 | cli 11052 | . . . . . . 7 | |
28 | 24, 26, 27 | wbr 3929 | . . . . . 6 |
29 | 9, 14, 28 | w3a 962 | . . . . 5 DECID |
30 | 29, 5, 17 | wrex 2417 | . . . 4 DECID |
31 | c1 7626 | . . . . . . . . 9 | |
32 | cfz 9795 | . . . . . . . . 9 | |
33 | 31, 6, 32 | co 5774 | . . . . . . . 8 |
34 | vf | . . . . . . . . 9 | |
35 | 34 | cv 1330 | . . . . . . . 8 |
36 | 33, 1, 35 | wf1o 5122 | . . . . . . 7 |
37 | cn 8725 | . . . . . . . . . . 11 | |
38 | cle 7806 | . . . . . . . . . . . . 13 | |
39 | 18, 6, 38 | wbr 3929 | . . . . . . . . . . . 12 |
40 | 18, 35 | cfv 5123 | . . . . . . . . . . . . 13 |
41 | 3, 40, 2 | csb 3003 | . . . . . . . . . . . 12 |
42 | 39, 41, 21 | cif 3474 | . . . . . . . . . . 11 |
43 | 16, 37, 42 | cmpt 3989 | . . . . . . . . . 10 |
44 | 15, 43, 31 | cseq 10223 | . . . . . . . . 9 |
45 | 6, 44 | cfv 5123 | . . . . . . . 8 |
46 | 26, 45 | wceq 1331 | . . . . . . 7 |
47 | 36, 46 | wa 103 | . . . . . 6 |
48 | 47, 34 | wex 1468 | . . . . 5 |
49 | 48, 5, 37 | wrex 2417 | . . . 4 |
50 | 30, 49 | wo 697 | . . 3 DECID |
51 | 50, 25 | cio 5086 | . 2 DECID |
52 | 4, 51 | wceq 1331 | 1 DECID |
Colors of variables: wff set class |
This definition is referenced by: sumeq1 11129 nfsum1 11130 nfsum 11131 sumeq2 11133 cbvsum 11134 zsumdc 11158 fsum3 11161 |
Copyright terms: Public domain | W3C validator |