Theorem sge0xrcl

Description: The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0xrcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0xrcl.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
Assertion	sge0xrcl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		sge0xrcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0xrcl.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
4	1 2	sge0cl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
5	3 4	sseldi	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ℝ* )