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 | ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vk | ⊢ 𝑘 | |
| 1 | cA | ⊢ 𝐴 | |
| 2 | cB | ⊢ 𝐵 | |
| 3 | 1 2 0 | cesum | ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 |
| 4 | cxrs | ⊢ ℝ*𝑠 | |
| 5 | cress | ⊢ ↾s | |
| 6 | cc0 | ⊢ 0 | |
| 7 | cicc | ⊢ [,] | |
| 8 | cpnf | ⊢ +∞ | |
| 9 | 6 8 7 | co | ⊢ ( 0 [,] +∞ ) |
| 10 | 4 9 5 | co | ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) |
| 11 | ctsu | ⊢ tsums | |
| 12 | 0 1 2 | cmpt | ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) |
| 13 | 10 12 11 | co | ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
| 14 | 13 | cuni | ⊢ ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |
| 15 | 3 14 | wceq | ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) |