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^ ⁡ ∅ = sup ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ℝ * <
13 12 mptru ⊢ sum^ ⁡ ∅ = sup ran ⁡ 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 ∈ 𝒫 ∅ ∩ Fin z = ∑ y ∈ x ∅ ⁡ y
17 14 16 ax-mp ⊢ z ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ↔ ∃ x ∈ 𝒫 ∅ ∩ Fin z = ∑ y ∈ x ∅ ⁡ y
18 17 biimpi ⊢ z ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y → ∃ x ∈ 𝒫 ∅ ∩ Fin z = ∑ y ∈ x ∅ ⁡ y
19 nfcv ⊢ Ⅎ _ x z
20 nfmpt1 ⊢ Ⅎ _ x x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y
21 20 nfrn ⊢ Ⅎ _ x ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y
22 19 21 nfel ⊢ Ⅎ x z ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y
23 nfv ⊢ Ⅎ x z = 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 ∈ 𝒫 ∅ ∩ Fin z = ∑ 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 0fi ⊢ ∅ ∈ 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 ∈ 𝒫 ∅ ∩ Fin 0 = ∑ y ∈ x ∅ ⁡ y
54 50 51 53 mp2an ⊢ ∃ x ∈ 𝒫 ∅ ∩ Fin 0 = ∑ y ∈ x ∅ ⁡ y
55 0re ⊢ 0 ∈ ℝ
56 15 elrnmpt ⊢ 0 ∈ ℝ → 0 ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ↔ ∃ x ∈ 𝒫 ∅ ∩ Fin 0 = ∑ y ∈ x ∅ ⁡ y
57 55 56 ax-mp ⊢ 0 ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ↔ ∃ x ∈ 𝒫 ∅ ∩ Fin 0 = ∑ 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 ⊢ ∀ z z ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ↔ z ∈ 0
63 dfcleq ⊢ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y = 0 ↔ ∀ z z ∈ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ↔ z ∈ 0
64 62 63 mpbir ⊢ ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y = 0
65 64 supeq1i ⊢ sup ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ℝ * < = sup 0 ℝ * <
66 xrltso ⊢ < Or ℝ *
67 0xr ⊢ 0 ∈ ℝ *
68 supsn ⊢ < Or ℝ * ∧ 0 ∈ ℝ * → sup 0 ℝ * < = 0
69 66 67 68 mp2an ⊢ sup 0 ℝ * < = 0
70 65 69 eqtri ⊢ sup ran ⁡ x ∈ 𝒫 ∅ ∩ Fin ⟼ ∑ y ∈ x ∅ ⁡ y ℝ * < = 0
71 13 70 eqtri ⊢ sum^ ⁡ ∅ = 0