Metamath Proof Explorer

Theorem sge00

Description: The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion sge00 ⊢sum^⁡∅=0

Proof

Step Hyp Ref Expression
1 0ex ⊢∅∈V
2 1 a1i ⊢⊤→∅∈V
3 f0 ⊢∅:∅⟶0+∞
4 3 a1i ⊢⊤→∅:∅⟶0+∞
5 noel ⊢¬+∞∈∅
6 5 a1i ⊢⊤→¬+∞∈∅
7 rn0 ⊢ran⁡∅=∅
8 7 eqcomi ⊢∅=ran⁡∅
9 8 a1i ⊢⊤→∅=ran⁡∅
10 6 9 neleqtrd ⊢⊤→¬+∞∈ran⁡∅
11 4 10 fge0iccico ⊢⊤→∅:∅⟶0+∞
12 2 11 sge0reval ⊢⊤→sum^⁡∅=supran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡yℝ*<
13 12 mptru ⊢sum^⁡∅=supran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡yℝ*<
14 vex ⊢z∈V
15 eqid ⊢x∈𝒫∅∩Fin⟼∑y∈x∅⁡y=x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
16 15 elrnmpt ⊢z∈V→z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔∃x∈𝒫∅∩Finz=∑y∈x∅⁡y
17 14 16 ax-mp ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔∃x∈𝒫∅∩Finz=∑y∈x∅⁡y
18 17 biimpi ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y→∃x∈𝒫∅∩Finz=∑y∈x∅⁡y
19 nfcv ⊢Ⅎ_xz
20 nfmpt1 ⊢Ⅎ_xx∈𝒫∅∩Fin⟼∑y∈x∅⁡y
21 20 nfrn ⊢Ⅎ_xran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
22 19 21 nfel ⊢Ⅎxz∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
23 nfv ⊢Ⅎxz=0
24 simpr ⊢x∈𝒫∅∩Fin∧z=∑y∈x∅⁡y→z=∑y∈x∅⁡y
25 elinel1 ⊢x∈𝒫∅∩Fin→x∈𝒫∅
26 pw0 ⊢𝒫∅=∅
27 26 eleq2i ⊢x∈𝒫∅↔x∈∅
28 27 biimpi ⊢x∈𝒫∅→x∈∅
29 25 28 syl ⊢x∈𝒫∅∩Fin→x∈∅
30 elsni ⊢x∈∅→x=∅
31 29 30 syl ⊢x∈𝒫∅∩Fin→x=∅
32 31 sumeq1d ⊢x∈𝒫∅∩Fin→∑y∈x∅⁡y=∑y∈∅∅⁡y
33 32 adantr ⊢x∈𝒫∅∩Fin∧z=∑y∈x∅⁡y→∑y∈x∅⁡y=∑y∈∅∅⁡y
34 sum0 ⊢∑y∈∅∅⁡y=0
35 34 a1i ⊢x∈𝒫∅∩Fin∧z=∑y∈x∅⁡y→∑y∈∅∅⁡y=0
36 24 33 35 3eqtrd ⊢x∈𝒫∅∩Fin∧z=∑y∈x∅⁡y→z=0
37 36 ex ⊢x∈𝒫∅∩Fin→z=∑y∈x∅⁡y→z=0
38 37 a1i ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y→x∈𝒫∅∩Fin→z=∑y∈x∅⁡y→z=0
39 22 23 38 rexlimd ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y→∃x∈𝒫∅∩Finz=∑y∈x∅⁡y→z=0
40 18 39 mpd ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y→z=0
41 velsn ⊢z∈0↔z=0
42 41 bicomi ⊢z=0↔z∈0
43 42 biimpi ⊢z=0→z∈0
44 40 43 syl ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y→z∈0
45 elsni ⊢z∈0→z=0
46 0elpw ⊢∅∈𝒫∅
47 0fin ⊢∅∈Fin
48 46 47 pm3.2i ⊢∅∈𝒫∅∧∅∈Fin
49 elin ⊢∅∈𝒫∅∩Fin↔∅∈𝒫∅∧∅∈Fin
50 48 49 mpbir ⊢∅∈𝒫∅∩Fin
51 34 eqcomi ⊢0=∑y∈∅∅⁡y
52 sumeq1 ⊢x=∅→∑y∈x∅⁡y=∑y∈∅∅⁡y
53 52 rspceeqv ⊢∅∈𝒫∅∩Fin∧0=∑y∈∅∅⁡y→∃x∈𝒫∅∩Fin0=∑y∈x∅⁡y
54 50 51 53 mp2an ⊢∃x∈𝒫∅∩Fin0=∑y∈x∅⁡y
55 0re ⊢0∈ℝ
56 15 elrnmpt ⊢0∈ℝ→0∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔∃x∈𝒫∅∩Fin0=∑y∈x∅⁡y
57 55 56 ax-mp ⊢0∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔∃x∈𝒫∅∩Fin0=∑y∈x∅⁡y
58 54 57 mpbir ⊢0∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
59 58 a1i ⊢z∈0→0∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
60 45 59 eqeltrd ⊢z∈0→z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y
61 44 60 impbii ⊢z∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔z∈0
62 61 ax-gen ⊢∀zz∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔z∈0
63 dfcleq ⊢ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y=0↔∀zz∈ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y↔z∈0
64 62 63 mpbir ⊢ran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡y=0
65 64 supeq1i ⊢supran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡yℝ*<=sup0ℝ*<
66 xrltso ⊢<Orℝ*
67 0xr ⊢0∈ℝ*
68 supsn ⊢<Orℝ*∧0∈ℝ*→sup0ℝ*<=0
69 66 67 68 mp2an ⊢sup0ℝ*<=0
70 65 69 eqtri ⊢supran⁡x∈𝒫∅∩Fin⟼∑y∈x∅⁡yℝ*<=0
71 13 70 eqtri ⊢sum^⁡∅=0