Metamath Proof Explorer

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 = ℝ 𝑠 * ↾ 𝑠 0 +∞
Assertion xrge0tsms2 ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → G tsums F ≈ 1 𝑜

Proof

Step Hyp Ref Expression
1 xrge0tsms2.g ⊢ G = ℝ 𝑠 * ↾ 𝑠 0 +∞
2 simpl ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → A ∈ V
3 simpr ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → F : A ⟶ 0 +∞
4 eqid ⊢ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ x ℝ * < = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ x ℝ * <
5 1 2 3 4 xrge0tsms ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → G tsums F = sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ x ℝ * <
6 xrltso ⊢ < Or ℝ *
7 6 supex ⊢ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ x ℝ * < ∈ V
8 7 ensn1 ⊢ sup ran ⁡ x ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ x ℝ * < ≈ 1 𝑜
9 5 8 eqbrtrdi ⊢ A ∈ V ∧ F : A ⟶ 0 +∞ → G tsums F ≈ 1 𝑜