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 | |- sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vk | |- k |
|
| 1 | cA | |- A |
|
| 2 | cB | |- B |
|
| 3 | 1 2 0 | cesum | |- sum* k e. A B |
| 4 | cxrs | |- RR*s |
|
| 5 | cress | |- |`s |
|
| 6 | cc0 | |- 0 |
|
| 7 | cicc | |- [,] |
|
| 8 | cpnf | |- +oo |
|
| 9 | 6 8 7 | co | |- ( 0 [,] +oo ) |
| 10 | 4 9 5 | co | |- ( RR*s |`s ( 0 [,] +oo ) ) |
| 11 | ctsu | |- tsums |
|
| 12 | 0 1 2 | cmpt | |- ( k e. A |-> B ) |
| 13 | 10 12 11 | co | |- ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) |
| 14 | 13 | cuni | |- U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) |
| 15 | 3 14 | wceq | |- sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) |