This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrge0tsms2

Description: Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set [ 0 , +oo ] ; a similar theorem is not true for RR* or RR or [ 0 , +oo ) . It is true for NN0 u. { +oo } , however, or more generally any additive submonoid of [ 0 , +oo ) with +oo adjoined. (Contributed by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis xrge0tsms2.g 
|- G = ( RR*s |`s ( 0 [,] +oo ) )
Assertion xrge0tsms2 
|- ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )

Proof

Step Hyp Ref Expression
1 xrge0tsms2.g 
 |-  G = ( RR*s |`s ( 0 [,] +oo ) )
2 simpl 
 |-  ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> A e. V )
3 simpr 
 |-  ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> F : A --> ( 0 [,] +oo ) )
4 eqid 
 |-  sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < )
5 1 2 3 4 xrge0tsms 
 |-  ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) = { sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } )
6 xrltso 
 |-  < Or RR*
7 6 supex 
 |-  sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) e. _V
8 7 ensn1 
 |-  { sup ( ran ( x e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` x ) ) ) , RR* , < ) } ~~ 1o
9 5 8 eqbrtrdi 
 |-  ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )