Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sum | 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. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.) |
Ref | Expression |
---|---|
df-sum |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | vk | . . 3 | |
4 | 1, 2, 3 | csu 9872 | . 2 |
5 | vm | . . . . . . . . 9 | |
6 | 5 | cv 1242 | . . . . . . . 8 |
7 | cuz 8473 | . . . . . . . 8 | |
8 | 6, 7 | cfv 4902 | . . . . . . 7 |
9 | 1, 8 | wss 2917 | . . . . . 6 |
10 | caddc 6892 | . . . . . . . 8 | |
11 | cc 6887 | . . . . . . . 8 | |
12 | vn | . . . . . . . . 9 | |
13 | cz 8245 | . . . . . . . . 9 | |
14 | 12 | cv 1242 | . . . . . . . . . . 11 |
15 | 14, 1 | wcel 1393 | . . . . . . . . . 10 |
16 | 3, 14, 2 | csb 2852 | . . . . . . . . . 10 |
17 | cc0 6889 | . . . . . . . . . 10 | |
18 | 15, 16, 17 | cif 3331 | . . . . . . . . 9 |
19 | 12, 13, 18 | cmpt 3818 | . . . . . . . 8 |
20 | 10, 11, 19, 6 | cseq 9211 | . . . . . . 7 |
21 | vx | . . . . . . . 8 | |
22 | 21 | cv 1242 | . . . . . . 7 |
23 | cli 9799 | . . . . . . 7 | |
24 | 20, 22, 23 | wbr 3764 | . . . . . 6 |
25 | 9, 24 | wa 97 | . . . . 5 |
26 | 25, 5, 13 | wrex 2307 | . . . 4 |
27 | c1 6890 | . . . . . . . . 9 | |
28 | cfz 8874 | . . . . . . . . 9 | |
29 | 27, 6, 28 | co 5512 | . . . . . . . 8 |
30 | vf | . . . . . . . . 9 | |
31 | 30 | cv 1242 | . . . . . . . 8 |
32 | 29, 1, 31 | wf1o 4901 | . . . . . . 7 |
33 | cn 7914 | . . . . . . . . . . 11 | |
34 | 14, 31 | cfv 4902 | . . . . . . . . . . . 12 |
35 | 3, 34, 2 | csb 2852 | . . . . . . . . . . 11 |
36 | 12, 33, 35 | cmpt 3818 | . . . . . . . . . 10 |
37 | 10, 11, 36, 27 | cseq 9211 | . . . . . . . . 9 |
38 | 6, 37 | cfv 4902 | . . . . . . . 8 |
39 | 22, 38 | wceq 1243 | . . . . . . 7 |
40 | 32, 39 | wa 97 | . . . . . 6 |
41 | 40, 30 | wex 1381 | . . . . 5 |
42 | 41, 5, 33 | wrex 2307 | . . . 4 |
43 | 26, 42 | wo 629 | . . 3 |
44 | 43, 21 | cio 4865 | . 2 |
45 | 4, 44 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: sumeq1 9874 nfsum1 9875 nfsum 9876 |
Copyright terms: Public domain | W3C validator |