Theorem sge0xrclmpt

Description: The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0xrclmpt.xph	⊢ Ⅎ 𝑥 𝜑
	sge0xrclmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0xrclmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion	sge0xrclmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		sge0xrclmpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0xrclmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0xrclmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5	1 2 3	sge0clmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
6	4 5	sseldi	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ℝ* )