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 34008
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 34007 . 2 class Σ*𝑘𝐴𝐵
5 cxrs 17546 . . . . 5 class *𝑠
6 cc0 11152 . . . . . 6 class 0
7 cpnf 11289 . . . . . 6 class +∞
8 cicc 13386 . . . . . 6 class [,]
96, 7, 8co 7430 . . . . 5 class (0[,]+∞)
10 cress 17273 . . . . 5 class s
115, 9, 10co 7430 . . . 4 class (ℝ*𝑠s (0[,]+∞))
123, 1, 2cmpt 5230 . . . 4 class (𝑘𝐴𝐵)
13 ctsu 24149 . . . 4 class tsums
1411, 12, 13co 7430 . . 3 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
1514cuni 4911 . 2 class ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
164, 15wceq 1536 1 wff Σ*𝑘𝐴𝐵 = ((ℝ*𝑠s (0[,]+∞)) tsums (𝑘𝐴𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  esumex  34009  esumcl  34010  esumeq12dvaf  34011  esumeq2  34016  nfesum1  34020  nfesum2  34021  cbvesum  34022  cbvesumv  34023  esumid  34024  esumval  34026  esumf1o  34030  esumsnf  34044  esumss  34052  esumpfinval  34055  esumpfinvalf  34056
  Copyright terms: Public domain W3C validator