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 . The variable 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 11449). (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 11280 | . 2 |
5 | vm | . . . . . . . . 9 | |
6 | 5 | cv 1341 | . . . . . . . 8 |
7 | cuz 9457 | . . . . . . . 8 | |
8 | 6, 7 | cfv 5182 | . . . . . . 7 |
9 | 1, 8 | wss 3111 | . . . . . 6 |
10 | vj | . . . . . . . . . 10 | |
11 | 10 | cv 1341 | . . . . . . . . 9 |
12 | 11, 1 | wcel 2135 | . . . . . . . 8 |
13 | 12 | wdc 824 | . . . . . . 7 DECID |
14 | 13, 10, 8 | wral 2442 | . . . . . 6 DECID |
15 | caddc 7747 | . . . . . . . 8 | |
16 | vn | . . . . . . . . 9 | |
17 | cz 9182 | . . . . . . . . 9 | |
18 | 16 | cv 1341 | . . . . . . . . . . 11 |
19 | 18, 1 | wcel 2135 | . . . . . . . . . 10 |
20 | 3, 18, 2 | csb 3040 | . . . . . . . . . 10 |
21 | cc0 7744 | . . . . . . . . . 10 | |
22 | 19, 20, 21 | cif 3515 | . . . . . . . . 9 |
23 | 16, 17, 22 | cmpt 4037 | . . . . . . . 8 |
24 | 15, 23, 6 | cseq 10370 | . . . . . . 7 |
25 | vx | . . . . . . . 8 | |
26 | 25 | cv 1341 | . . . . . . 7 |
27 | cli 11205 | . . . . . . 7 | |
28 | 24, 26, 27 | wbr 3976 | . . . . . 6 |
29 | 9, 14, 28 | w3a 967 | . . . . 5 DECID |
30 | 29, 5, 17 | wrex 2443 | . . . 4 DECID |
31 | c1 7745 | . . . . . . . . 9 | |
32 | cfz 9935 | . . . . . . . . 9 | |
33 | 31, 6, 32 | co 5836 | . . . . . . . 8 |
34 | vf | . . . . . . . . 9 | |
35 | 34 | cv 1341 | . . . . . . . 8 |
36 | 33, 1, 35 | wf1o 5181 | . . . . . . 7 |
37 | cn 8848 | . . . . . . . . . . 11 | |
38 | cle 7925 | . . . . . . . . . . . . 13 | |
39 | 18, 6, 38 | wbr 3976 | . . . . . . . . . . . 12 |
40 | 18, 35 | cfv 5182 | . . . . . . . . . . . . 13 |
41 | 3, 40, 2 | csb 3040 | . . . . . . . . . . . 12 |
42 | 39, 41, 21 | cif 3515 | . . . . . . . . . . 11 |
43 | 16, 37, 42 | cmpt 4037 | . . . . . . . . . 10 |
44 | 15, 43, 31 | cseq 10370 | . . . . . . . . 9 |
45 | 6, 44 | cfv 5182 | . . . . . . . 8 |
46 | 26, 45 | wceq 1342 | . . . . . . 7 |
47 | 36, 46 | wa 103 | . . . . . 6 |
48 | 47, 34 | wex 1479 | . . . . 5 |
49 | 48, 5, 37 | wrex 2443 | . . . 4 |
50 | 30, 49 | wo 698 | . . 3 DECID |
51 | 50, 25 | cio 5145 | . 2 DECID |
52 | 4, 51 | wceq 1342 | 1 DECID |
Colors of variables: wff set class |
This definition is referenced by: sumeq1 11282 nfsum1 11283 nfsum 11284 sumeq2 11286 cbvsum 11287 zsumdc 11311 fsum3 11314 |
Copyright terms: Public domain | W3C validator |