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

Metamath Proof Explorer

Theorem xrge0tsmseq

Description: Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 24-Mar-2017)

		Ref	Expression
	Hypotheses	xrge0tsmseq.g	\|- G = ( RR*s \|`s ( 0 [,] +oo ) )
		xrge0tsmseq.a	\|- ( ph -> A e. V )
		xrge0tsmseq.f	\|- ( ph -> F : A --> ( 0 [,] +oo ) )
		xrge0tsmseq.h	\|- ( ph -> C e. ( G tsums F ) )
	Assertion	xrge0tsmseq	\|- ( ph -> C = U. ( G tsums F ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	\|- G = ( RR*s \|`s ( 0 [,] +oo ) )
2		xrge0tsmseq.a	\|- ( ph -> A e. V )
3		xrge0tsmseq.f	\|- ( ph -> F : A --> ( 0 [,] +oo ) )
4		xrge0tsmseq.h	\|- ( ph -> C e. ( G tsums F ) )
5	1	xrge0tsms2	\|- ( ( A e. V /\ F : A --> ( 0 [,] +oo ) ) -> ( G tsums F ) ~~ 1o )
6	2 3 5	syl2anc	\|- ( ph -> ( G tsums F ) ~~ 1o )
7		en1eqsn	\|- ( ( C e. ( G tsums F ) /\ ( G tsums F ) ~~ 1o ) -> ( G tsums F ) = { C } )
8	4 6 7	syl2anc	\|- ( ph -> ( G tsums F ) = { C } )
9	8	unieqd	\|- ( ph -> U. ( G tsums F ) = U. { C } )
10		unisng	\|- ( C e. ( G tsums F ) -> U. { C } = C )
11	4 10	syl	\|- ( ph -> U. { C } = C )
12	9 11	eqtr2d	\|- ( ph -> C = U. ( G tsums F ) )