Definition df-esum 34205

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.)

Assertion

Ref	Expression
df-esum	⊢ Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))

Detailed syntax breakdown of Definition df-esum

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		vk	. . 3 setvar 𝑘
4	1, 2, 3	cesum 34204	. 2 class Σ*𝑘 ∈ 𝐴𝐵
5		cxrs 17433	. . . . 5 class ℝ*𝑠
6		cc0 11038	. . . . . 6 class 0
7		cpnf 11175	. . . . . 6 class +∞
8		cicc 13276	. . . . . 6 class [,]
9	6, 7, 8	co 7368	. . . . 5 class (0[,]+∞)
10		cress 17169	. . . . 5 class ↾s
11	5, 9, 10	co 7368	. . . 4 class (ℝ*𝑠 ↾s (0[,]+∞))
12	3, 1, 2	cmpt 5181	. . . 4 class (𝑘 ∈ 𝐴 ↦ 𝐵)
13		ctsu 24082	. . . 4 class tsums
14	11, 12, 13	co 7368	. . 3 class ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
15	14	cuni 4865	. 2 class ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))
16	4, 15	wceq 1542	1 wff Σ*𝑘 ∈ 𝐴𝐵 = ∪ ((ℝ*𝑠 ↾s (0[,]+∞)) tsums (𝑘 ∈ 𝐴 ↦ 𝐵))

This definition is referenced by:  esumex  34206  esumcl  34207  esumeq12dvaf  34208  esumeq2  34213  nfesum1  34217  nfesum2  34218  cbvesum  34219  cbvesumv  34220  esumid  34221  esumval  34223  esumf1o  34227  esumsnf  34241  esumss  34249  esumpfinval  34252  esumpfinvalf  34253