Definition df-esum 30090

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

Assertion

Ref	Expression
df-esum	|- Σ* k e. A B = U. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )

Detailed syntax breakdown of Definition df-esum

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		vk	. . 3 setvar k
4	1, 2, 3	cesum 30089	. 2 class Σ* k e. A B
5		cxrs 16160	. . . . 5 class RR*s
6		cc0 9936	. . . . . 6 class 0
7		cpnf 10071	. . . . . 6 class +oo
8		cicc 12178	. . . . . 6 class [,]
9	6, 7, 8	co 6650	. . . . 5 class ( 0 [,] +oo )
10		cress 15858	. . . . 5 class ↾s
11	5, 9, 10	co 6650	. . . 4 class ( RR*s ↾s ( 0 [,] +oo ) )
12	3, 1, 2	cmpt 4729	. . . 4 class ( k e. A |-> B )
13		ctsu 21929	. . . 4 class tsums
14	11, 12, 13	co 6650	. . 3 class ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
15	14	cuni 4436	. 2 class U. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
16	4, 15	wceq 1483	1 wff Σ* k e. A B = U. ( ( RR*s ↾s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )

This definition is referenced by:  esumex  30091  esumcl  30092  esumeq12dvaf  30093  esumeq2  30098  nfesum1  30102  nfesum2  30103  cbvesum  30104  esumid  30106  esumval  30108  esumf1o  30112  esumsnf  30126  esumss  30134  esumpfinval  30137  esumpfinvalf  30138