Theorem sge0clmpt

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

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

Proof

Step	Hyp	Ref	Expression
1		sge0clmpt.xph	⊢ Ⅎ 𝑥 𝜑
2		sge0clmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0clmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5	1 3 4	fmptdf	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
6	2 5	sge0cl	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ ( 0 [,] +∞ ) )