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	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
	xrge0tsmseq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	xrge0tsmseq.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
	xrge0tsmseq.h	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 tsums 𝐹 ) )
Assertion	xrge0tsmseq	⊢ ( 𝜑 → 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsmseq.g	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		xrge0tsmseq.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		xrge0tsmseq.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
4		xrge0tsmseq.h	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐺 tsums 𝐹 ) )
5	1	xrge0tsms2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → ( 𝐺 tsums 𝐹 ) ≈ 1o )
6	2 3 5	syl2anc	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ≈ 1o )
7		en1eqsn	⊢ ( ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ∧ ( 𝐺 tsums 𝐹 ) ≈ 1o ) → ( 𝐺 tsums 𝐹 ) = { 𝐶 } )
8	4 6 7	syl2anc	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = { 𝐶 } )
9	8	unieqd	⊢ ( 𝜑 → ∪ ( 𝐺 tsums 𝐹 ) = ∪ { 𝐶 } )
10		unisng	⊢ ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) → ∪ { 𝐶 } = 𝐶 )
11	4 10	syl	⊢ ( 𝜑 → ∪ { 𝐶 } = 𝐶 )
12	9 11	eqtr2d	⊢ ( 𝜑 → 𝐶 = ∪ ( 𝐺 tsums 𝐹 ) )