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 ${⊢}\mathrm{sum^}\left(\varnothing \right)=0$

Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 1 a1i ${⊢}\top \to \varnothing \in \mathrm{V}$
3 f0 ${⊢}\varnothing :\varnothing ⟶\left[0,\mathrm{+\infty }\right]$
4 3 a1i ${⊢}\top \to \varnothing :\varnothing ⟶\left[0,\mathrm{+\infty }\right]$
5 noel ${⊢}¬\mathrm{+\infty }\in \varnothing$
6 5 a1i ${⊢}\top \to ¬\mathrm{+\infty }\in \varnothing$
7 rn0 ${⊢}\mathrm{ran}\varnothing =\varnothing$
8 7 eqcomi ${⊢}\varnothing =\mathrm{ran}\varnothing$
9 8 a1i ${⊢}\top \to \varnothing =\mathrm{ran}\varnothing$
10 6 9 neleqtrd ${⊢}\top \to ¬\mathrm{+\infty }\in \mathrm{ran}\varnothing$
11 4 10 fge0iccico ${⊢}\top \to \varnothing :\varnothing ⟶\left[0,\mathrm{+\infty }\right)$
12 2 11 sge0reval ${⊢}\top \to \mathrm{sum^}\left(\varnothing \right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right),{ℝ}^{*},<\right)$
13 12 mptru ${⊢}\mathrm{sum^}\left(\varnothing \right)=sup\left(\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right),{ℝ}^{*},<\right)$
14 vex ${⊢}{z}\in \mathrm{V}$
15 eqid ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)=\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
16 15 elrnmpt ${⊢}{z}\in \mathrm{V}\to \left({z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
17 14 16 ax-mp ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
18 17 biimpi ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to \exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
20 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
21 20 nfrn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
22 19 21 nfel ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
23 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}=0$
24 simpr ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge {z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to {z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
25 elinel1 ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to {x}\in 𝒫\varnothing$
26 pw0 ${⊢}𝒫\varnothing =\left\{\varnothing \right\}$
27 26 eleq2i ${⊢}{x}\in 𝒫\varnothing ↔{x}\in \left\{\varnothing \right\}$
28 27 biimpi ${⊢}{x}\in 𝒫\varnothing \to {x}\in \left\{\varnothing \right\}$
29 25 28 syl ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to {x}\in \left\{\varnothing \right\}$
30 elsni ${⊢}{x}\in \left\{\varnothing \right\}\to {x}=\varnothing$
31 29 30 syl ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to {x}=\varnothing$
32 31 sumeq1d ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to \sum _{{y}\in {x}}\varnothing \left({y}\right)=\sum _{{y}\in \varnothing }\varnothing \left({y}\right)$
33 32 adantr ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge {z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to \sum _{{y}\in {x}}\varnothing \left({y}\right)=\sum _{{y}\in \varnothing }\varnothing \left({y}\right)$
34 sum0 ${⊢}\sum _{{y}\in \varnothing }\varnothing \left({y}\right)=0$
35 34 a1i ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge {z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to \sum _{{y}\in \varnothing }\varnothing \left({y}\right)=0$
36 24 33 35 3eqtrd ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge {z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to {z}=0$
37 36 ex ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to \left({z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\to {z}=0\right)$
38 37 a1i ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to \left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to \left({z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\to {z}=0\right)\right)$
39 22 23 38 rexlimd ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to \left(\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{z}=\sum _{{y}\in {x}}\varnothing \left({y}\right)\to {z}=0\right)$
40 18 39 mpd ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to {z}=0$
41 velsn ${⊢}{z}\in \left\{0\right\}↔{z}=0$
42 41 bicomi ${⊢}{z}=0↔{z}\in \left\{0\right\}$
43 42 biimpi ${⊢}{z}=0\to {z}\in \left\{0\right\}$
44 40 43 syl ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)\to {z}\in \left\{0\right\}$
45 elsni ${⊢}{z}\in \left\{0\right\}\to {z}=0$
46 0elpw ${⊢}\varnothing \in 𝒫\varnothing$
47 0fin ${⊢}\varnothing \in \mathrm{Fin}$
48 46 47 pm3.2i ${⊢}\left(\varnothing \in 𝒫\varnothing \wedge \varnothing \in \mathrm{Fin}\right)$
49 elin ${⊢}\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)↔\left(\varnothing \in 𝒫\varnothing \wedge \varnothing \in \mathrm{Fin}\right)$
50 48 49 mpbir ${⊢}\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)$
51 34 eqcomi ${⊢}0=\sum _{{y}\in \varnothing }\varnothing \left({y}\right)$
52 sumeq1 ${⊢}{x}=\varnothing \to \sum _{{y}\in {x}}\varnothing \left({y}\right)=\sum _{{y}\in \varnothing }\varnothing \left({y}\right)$
53 52 rspceeqv ${⊢}\left(\varnothing \in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge 0=\sum _{{y}\in \varnothing }\varnothing \left({y}\right)\right)\to \exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
54 50 51 53 mp2an ${⊢}\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
55 0re ${⊢}0\in ℝ$
56 15 elrnmpt ${⊢}0\in ℝ\to \left(0\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
57 55 56 ax-mp ${⊢}0\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}0=\sum _{{y}\in {x}}\varnothing \left({y}\right)$
58 54 57 mpbir ${⊢}0\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
59 58 a1i ${⊢}{z}\in \left\{0\right\}\to 0\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
60 45 59 eqeltrd ${⊢}{z}\in \left\{0\right\}\to {z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)$
61 44 60 impbii ${⊢}{z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔{z}\in \left\{0\right\}$
62 61 ax-gen ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔{z}\in \left\{0\right\}\right)$
63 dfcleq ${⊢}\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)=\left\{0\right\}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in \mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)↔{z}\in \left\{0\right\}\right)$
64 62 63 mpbir ${⊢}\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right)=\left\{0\right\}$
65 64 supeq1i ${⊢}sup\left(\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right),{ℝ}^{*},<\right)=sup\left(\left\{0\right\},{ℝ}^{*},<\right)$
66 xrltso ${⊢}<\mathrm{Or}{ℝ}^{*}$
67 0xr ${⊢}0\in {ℝ}^{*}$
68 supsn ${⊢}\left(<\mathrm{Or}{ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
69 66 67 68 mp2an ${⊢}sup\left(\left\{0\right\},{ℝ}^{*},<\right)=0$
70 65 69 eqtri ${⊢}sup\left(\mathrm{ran}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)⟼\sum _{{y}\in {x}}\varnothing \left({y}\right)\right),{ℝ}^{*},<\right)=0$
71 13 70 eqtri ${⊢}\mathrm{sum^}\left(\varnothing \right)=0$