![]() |
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 30859 | . 2 class Σ*𝑘 ∈ 𝐴𝐵 |
5 | cxrs 16590 | . . . . 5 class ℝ*𝑠 | |
6 | cc0 10372 | . . . . . 6 class 0 | |
7 | cpnf 10507 | . . . . . 6 class +∞ | |
8 | cicc 12580 | . . . . . 6 class [,] | |
9 | 6, 7, 8 | co 7007 | . . . . 5 class (0[,]+∞) |
10 | cress 16301 | . . . . 5 class ↾s | |
11 | 5, 9, 10 | co 7007 | . . . 4 class (ℝ*𝑠 ↾s (0[,]+∞)) |
12 | 3, 1, 2 | cmpt 5035 | . . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵) |
13 | ctsu 22405 | . . . 4 class tsums | |
14 | 11, 12, 13 | co 7007 | . . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
15 | 14 | cuni 4739 | . 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
16 | 4, 15 | wceq 1520 | 1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵)) |
Colors of variables: wff setvar class |
This definition is referenced by: esumex 30861 esumcl 30862 esumeq12dvaf 30863 esumeq2 30868 nfesum1 30872 nfesum2 30873 cbvesum 30874 esumid 30876 esumval 30878 esumf1o 30882 esumsnf 30896 esumss 30904 esumpfinval 30907 esumpfinvalf 30908 |
Copyright terms: Public domain | W3C validator |