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 )