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 ⊢ 𝐺 = ( ℝ*𝑠 ↾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 𝐹 ) )