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	⊢ 𝐺 = ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) )
	Assertion	xrge0tsms2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → ( 𝐺 tsums 𝐹 ) ≈ 1_o )

Proof

Step	Hyp	Ref	Expression
1		xrge0tsms2.g	⊢ 𝐺 = ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) )
2		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → 𝐴 ∈ 𝑉 )
3		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
4		eqid	⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑥 ) ) ) , ℝ^* , < ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑥 ) ) ) , ℝ^* , < )
5	1 2 3 4	xrge0tsms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → ( 𝐺 tsums 𝐹 ) = { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑥 ) ) ) , ℝ^* , < ) } )
6		xrltso	⊢ < Or ℝ^*
7	6	supex	⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑥 ) ) ) , ℝ^* , < ) ∈ V
8	7	ensn1	⊢ { sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σ_g ( 𝐹 ↾ 𝑥 ) ) ) , ℝ^* , < ) } ≈ 1_o
9	5 8	eqbrtrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) → ( 𝐺 tsums 𝐹 ) ≈ 1_o )

Metamath Proof Explorer

Theorem xrge0tsms2

Proof