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 \in V \land F : A ⟶ [0, +∞]) \to (G tsums F) \approx 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		xrge0tsms2.g	$⊢ G = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
2		simpl	$⊢ (A \in V \land F : A ⟶ [0, +∞]) \to A \in V$
3		simpr	$⊢ (A \in V \land F : A ⟶ [0, +∞]) \to F : A ⟶ [0, +∞]$
4		eqid	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)$
5	1 2 3 4	xrge0tsms	$⊢ (A \in V \land F : A ⟶ [0, +∞]) \to G tsums F = \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)\}$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	supex	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) \in V$
8	7	ensn1	$⊢ \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)\} \approx 1_{𝑜}$
9	5 8	eqbrtrdi	$⊢ (A \in V \land F : A ⟶ [0, +∞]) \to (G tsums F) \approx 1_{𝑜}$

Metamath Proof Explorer

Theorem xrge0tsms2

Proof