Metamath Proof Explorer

Definition df-sumge0

Description: Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020) $.

Ref Expression
Assertion df-sumge0 ⊢ sum^ = x ∈ V ⟼ if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <

Detailed syntax breakdown

Step Hyp Ref Expression
0 csumge0 class sum^
1 vx setvar x
2 cvv class V
3 cpnf class +∞
4 1 cv setvar x
5 4 crn class ran ⁡ x
6 3 5 wcel wff +∞ ∈ ran ⁡ x
7 vy setvar y
8 4 cdm class dom ⁡ x
9 8 cpw class 𝒫 dom ⁡ x
10 cfn class Fin
11 9 10 cin class 𝒫 dom ⁡ x ∩ Fin
12 vw setvar w
13 7 cv setvar y
14 12 cv setvar w
15 14 4 cfv class x ⁡ w
16 13 15 12 csu class ∑ w ∈ y x ⁡ w
17 7 11 16 cmpt class y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w
18 17 crn class ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w
19 cxr class ℝ *
20 clt class <
21 18 19 20 csup class sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <
22 6 3 21 cif class if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <
23 1 2 22 cmpt class x ∈ V ⟼ if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <
24 0 23 wceq wff sum^ = x ∈ V ⟼ if +∞ ∈ ran ⁡ x +∞ sup ran ⁡ y ∈ 𝒫 dom ⁡ x ∩ Fin ⟼ ∑ w ∈ y x ⁡ w ℝ * <