Metamath Proof Explorer


Definition df-esum

Description: Define a short-hand for the possibly infinite sum over the extended nonnegative reals. sum* is relying on the properties of the tsums , developped by Mario Carneiro. (Contributed by Thierry Arnoux, 21-Sep-2016)

Ref Expression
Assertion df-esum *kAB=𝑠*𝑠0+∞tsumskAB

Detailed syntax breakdown

Step Hyp Ref Expression
0 vk setvark
1 cA classA
2 cB classB
3 1 2 0 cesum class*kAB
4 cxrs class𝑠*
5 cress class𝑠
6 cc0 class0
7 cicc class.
8 cpnf class+∞
9 6 8 7 co class0+∞
10 4 9 5 co class𝑠*𝑠0+∞
11 ctsu classtsums
12 0 1 2 cmpt classkAB
13 10 12 11 co class𝑠*𝑠0+∞tsumskAB
14 13 cuni class𝑠*𝑠0+∞tsumskAB
15 3 14 wceq wff*kAB=𝑠*𝑠0+∞tsumskAB