| Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-esum | Structured version Visualization version GIF version | ||
| Description: Define a short-hand for the possibly infinite sum over the extended nonnegative reals. Σ* is relying on the properties of the tsums, developed by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016.) |
| Ref | Expression |
|---|---|
| df-esum | ⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cB | . . 3 class 𝐵 | |
| 3 | vk | . . 3 setvar 𝑘 | |
| 4 | 1, 2, 3 | cesum 34028 | . 2 class Σ*𝑘 ∈ 𝐴𝐵 |
| 5 | cxrs 17545 | . . . . 5 class ℝ*𝑠 | |
| 6 | cc0 11155 | . . . . . 6 class 0 | |
| 7 | cpnf 11292 | . . . . . 6 class +∞ | |
| 8 | cicc 13390 | . . . . . 6 class [,] | |
| 9 | 6, 7, 8 | co 7431 | . . . . 5 class (0[,]+∞) |
| 10 | cress 17274 | . . . . 5 class ↾s | |
| 11 | 5, 9, 10 | co 7431 | . . . 4 class (ℝ*𝑠 ↾s (0[,]+∞)) |
| 12 | 3, 1, 2 | cmpt 5225 | . . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵) |
| 13 | ctsu 24134 | . . . 4 class tsums | |
| 14 | 11, 12, 13 | co 7431 | . . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
| 15 | 14 | cuni 4907 | . 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
| 16 | 4, 15 | wceq 1540 | 1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: esumex 34030 esumcl 34031 esumeq12dvaf 34032 esumeq2 34037 nfesum1 34041 nfesum2 34042 cbvesum 34043 cbvesumv 34044 esumid 34045 esumval 34047 esumf1o 34051 esumsnf 34065 esumss 34073 esumpfinval 34076 esumpfinvalf 34077 |
| Copyright terms: Public domain | W3C validator |