Theorem sge0ge0mpt

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

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

Proof

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