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 
 |-  (/) e. _V
2 1 a1i 
 |-  ( T. -> (/) e. _V )
3 f0 
 |-  (/) : (/) --> ( 0 [,] +oo )
4 3 a1i 
 |-  ( T. -> (/) : (/) --> ( 0 [,] +oo ) )
5 noel 
 |-  -. +oo e. (/)
6 5 a1i 
 |-  ( T. -> -. +oo e. (/) )
7 rn0 
 |-  ran (/) = (/)
8 7 eqcomi 
 |-  (/) = ran (/)
9 8 a1i 
 |-  ( T. -> (/) = ran (/) )
10 6 9 neleqtrd 
 |-  ( T. -> -. +oo e. ran (/) )
11 4 10 fge0iccico 
 |-  ( T. -> (/) : (/) --> ( 0 [,) +oo ) )
12 2 11 sge0reval 
 |-  ( T. -> ( sum^ ` (/) ) = sup ( ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) , RR* , < ) )
13 12 mptru 
 |-  ( sum^ ` (/) ) = sup ( ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) , RR* , < )
14 vex 
 |-  z e. _V
15 eqid 
 |-  ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) = ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) )
16 15 elrnmpt 
 |-  ( z e. _V -> ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> E. x e. ( ~P (/) i^i Fin ) z = sum_ y e. x ( (/) ` y ) ) )
17 14 16 ax-mp 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> E. x e. ( ~P (/) i^i Fin ) z = sum_ y e. x ( (/) ` y ) )
18 17 biimpi 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) -> E. x e. ( ~P (/) i^i Fin ) z = sum_ y e. x ( (/) ` y ) )
19 nfcv 
 |-  F/_ x z
20 nfmpt1 
 |-  F/_ x ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) )
21 20 nfrn 
 |-  F/_ x ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) )
22 19 21 nfel 
 |-  F/ x z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) )
23 nfv 
 |-  F/ x z = 0
24 simpr 
 |-  ( ( x e. ( ~P (/) i^i Fin ) /\ z = sum_ y e. x ( (/) ` y ) ) -> z = sum_ y e. x ( (/) ` y ) )
25 elinel1 
 |-  ( x e. ( ~P (/) i^i Fin ) -> x e. ~P (/) )
26 pw0 
 |-  ~P (/) = { (/) }
27 26 eleq2i 
 |-  ( x e. ~P (/) <-> x e. { (/) } )
28 27 biimpi 
 |-  ( x e. ~P (/) -> x e. { (/) } )
29 25 28 syl 
 |-  ( x e. ( ~P (/) i^i Fin ) -> x e. { (/) } )
30 elsni 
 |-  ( x e. { (/) } -> x = (/) )
31 29 30 syl 
 |-  ( x e. ( ~P (/) i^i Fin ) -> x = (/) )
32 31 sumeq1d 
 |-  ( x e. ( ~P (/) i^i Fin ) -> sum_ y e. x ( (/) ` y ) = sum_ y e. (/) ( (/) ` y ) )
33 32 adantr 
 |-  ( ( x e. ( ~P (/) i^i Fin ) /\ z = sum_ y e. x ( (/) ` y ) ) -> sum_ y e. x ( (/) ` y ) = sum_ y e. (/) ( (/) ` y ) )
34 sum0 
 |-  sum_ y e. (/) ( (/) ` y ) = 0
35 34 a1i 
 |-  ( ( x e. ( ~P (/) i^i Fin ) /\ z = sum_ y e. x ( (/) ` y ) ) -> sum_ y e. (/) ( (/) ` y ) = 0 )
36 24 33 35 3eqtrd 
 |-  ( ( x e. ( ~P (/) i^i Fin ) /\ z = sum_ y e. x ( (/) ` y ) ) -> z = 0 )
37 36 ex 
 |-  ( x e. ( ~P (/) i^i Fin ) -> ( z = sum_ y e. x ( (/) ` y ) -> z = 0 ) )
38 37 a1i 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) -> ( x e. ( ~P (/) i^i Fin ) -> ( z = sum_ y e. x ( (/) ` y ) -> z = 0 ) ) )
39 22 23 38 rexlimd 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) -> ( E. x e. ( ~P (/) i^i Fin ) z = sum_ y e. x ( (/) ` y ) -> z = 0 ) )
40 18 39 mpd 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) -> z = 0 )
41 velsn 
 |-  ( z e. { 0 } <-> z = 0 )
42 41 bicomi 
 |-  ( z = 0 <-> z e. { 0 } )
43 42 biimpi 
 |-  ( z = 0 -> z e. { 0 } )
44 40 43 syl 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) -> z e. { 0 } )
45 elsni 
 |-  ( z e. { 0 } -> z = 0 )
46 0elpw 
 |-  (/) e. ~P (/)
47 0fi 
 |-  (/) e. Fin
48 46 47 pm3.2i 
 |-  ( (/) e. ~P (/) /\ (/) e. Fin )
49 elin 
 |-  ( (/) e. ( ~P (/) i^i Fin ) <-> ( (/) e. ~P (/) /\ (/) e. Fin ) )
50 48 49 mpbir 
 |-  (/) e. ( ~P (/) i^i Fin )
51 34 eqcomi 
 |-  0 = sum_ y e. (/) ( (/) ` y )
52 sumeq1 
 |-  ( x = (/) -> sum_ y e. x ( (/) ` y ) = sum_ y e. (/) ( (/) ` y ) )
53 52 rspceeqv 
 |-  ( ( (/) e. ( ~P (/) i^i Fin ) /\ 0 = sum_ y e. (/) ( (/) ` y ) ) -> E. x e. ( ~P (/) i^i Fin ) 0 = sum_ y e. x ( (/) ` y ) )
54 50 51 53 mp2an 
 |-  E. x e. ( ~P (/) i^i Fin ) 0 = sum_ y e. x ( (/) ` y )
55 0re 
 |-  0 e. RR
56 15 elrnmpt 
 |-  ( 0 e. RR -> ( 0 e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> E. x e. ( ~P (/) i^i Fin ) 0 = sum_ y e. x ( (/) ` y ) ) )
57 55 56 ax-mp 
 |-  ( 0 e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> E. x e. ( ~P (/) i^i Fin ) 0 = sum_ y e. x ( (/) ` y ) )
58 54 57 mpbir 
 |-  0 e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) )
59 58 a1i 
 |-  ( z e. { 0 } -> 0 e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) )
60 45 59 eqeltrd 
 |-  ( z e. { 0 } -> z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) )
61 44 60 impbii 
 |-  ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> z e. { 0 } )
62 61 ax-gen 
 |-  A. z ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> z e. { 0 } )
63 dfcleq 
 |-  ( ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) = { 0 } <-> A. z ( z e. ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) <-> z e. { 0 } ) )
64 62 63 mpbir 
 |-  ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) = { 0 }
65 64 supeq1i 
 |-  sup ( ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) , RR* , < ) = sup ( { 0 } , RR* , < )
66 xrltso 
 |-  < Or RR*
67 0xr 
 |-  0 e. RR*
68 supsn 
 |-  ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
69 66 67 68 mp2an 
 |-  sup ( { 0 } , RR* , < ) = 0
70 65 69 eqtri 
 |-  sup ( ran ( x e. ( ~P (/) i^i Fin ) |-> sum_ y e. x ( (/) ` y ) ) , RR* , < ) = 0
71 13 70 eqtri 
 |-  ( sum^ ` (/) ) = 0