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 = ℝ 𝑠 * ↾ 𝑠 0 +∞
xrge0tsmseq.a ⊢ φ → A ∈ V
xrge0tsmseq.f ⊢ φ → F : A ⟶ 0 +∞
xrge0tsmseq.h ⊢ φ → C ∈ G tsums F
Assertion xrge0tsmseq ⊢ φ → C = ⋃ G tsums F

Proof

Step Hyp Ref Expression
1 xrge0tsmseq.g ⊢ G = ℝ 𝑠 * ↾ 𝑠 0 +∞
2 xrge0tsmseq.a ⊢ φ → A ∈ V
3 xrge0tsmseq.f ⊢ φ → F : A ⟶ 0 +∞
4 xrge0tsmseq.h ⊢ φ → C ∈ G tsums F
5 1 xrge0tsms2 ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → G tsums F ≈ 1 𝑜
6 2 3 5 syl2anc ⊢ φ → G tsums F ≈ 1 𝑜
7 en1eqsn ⊢ C ∈ G tsums F ∧ G tsums F ≈ 1 𝑜 → G tsums F = C
8 4 6 7 syl2anc ⊢ φ → G tsums F = C
9 8 unieqd ⊢ φ → ⋃ G tsums F = ⋃ C
10 unisng ⊢ C ∈ G tsums F → ⋃ C = C
11 4 10 syl ⊢ φ → ⋃ C = C
12 9 11 eqtr2d ⊢ φ → C = ⋃ G tsums F