Description: Define a short-hand for the possibly infinite sum over the extended nonnegative reals. sum* is relying on the properties of the tsums , developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-esum | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | vk | |
|
1 | cA | |
|
2 | cB | |
|
3 | 1 2 0 | cesum | |
4 | cxrs | |
|
5 | cress | |
|
6 | cc0 | |
|
7 | cicc | |
|
8 | cpnf | |
|
9 | 6 8 7 | co | |
10 | 4 9 5 | co | |
11 | ctsu | |
|
12 | 0 1 2 | cmpt | |
13 | 10 12 11 | co | |
14 | 13 | cuni | |
15 | 3 14 | wceq | |