![]() |
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, developped 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 33777 | . 2 class Σ*𝑘 ∈ 𝐴𝐵 |
5 | cxrs 17485 | . . . . 5 class ℝ*𝑠 | |
6 | cc0 11140 | . . . . . 6 class 0 | |
7 | cpnf 11277 | . . . . . 6 class +∞ | |
8 | cicc 13362 | . . . . . 6 class [,] | |
9 | 6, 7, 8 | co 7419 | . . . . 5 class (0[,]+∞) |
10 | cress 17212 | . . . . 5 class ↾s | |
11 | 5, 9, 10 | co 7419 | . . . 4 class (ℝ*𝑠 ↾s (0[,]+∞)) |
12 | 3, 1, 2 | cmpt 5232 | . . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵) |
13 | ctsu 24074 | . . . 4 class tsums | |
14 | 11, 12, 13 | co 7419 | . . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
15 | 14 | cuni 4909 | . 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
16 | 4, 15 | wceq 1533 | 1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: esumex 33779 esumcl 33780 esumeq12dvaf 33781 esumeq2 33786 nfesum1 33790 nfesum2 33791 cbvesum 33792 esumid 33794 esumval 33796 esumf1o 33800 esumsnf 33814 esumss 33822 esumpfinval 33825 esumpfinvalf 33826 |
Copyright terms: Public domain | W3C validator |