Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-esum Structured version   Visualization version   GIF version

Definition df-esum 34029
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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 vk . . 3 setvar 𝑘
41, 2, 3cesum 34028 . 2 class Σ*𝑘𝐴𝐵
5 cxrs 17545 . . . . 5 class *𝑠
6 cc0 11155 . . . . . 6 class 0
7 cpnf 11292 . . . . . 6 class +∞
8 cicc 13390 . . . . . 6 class [,]
96, 7, 8co 7431 . . . . 5 class (0[,]+∞)
10 cress 17274 . . . . 5 class s
115, 9, 10co 7431 . . . 4 class (ℝ*𝑠s (0[,]+∞))
123, 1, 2cmpt 5225 . . . 4 class (𝑘𝐴𝐵)
13 ctsu 24134 . . . 4 class tsums
1411, 12, 13co 7431 . . 3 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
1514cuni 4907 . 2 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
164, 15wceq 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