Theorem sge0ge0

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

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

Proof

Step	Hyp	Ref	Expression
1		sge0ge0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0ge0.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		0xr	⊢ 0 ∈ ℝ*
4	3	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6	5	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
7	1 2	sge0cl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
8		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) ) → 0 ≤ ( Σ^ ‘ 𝐹 ) )
9	4 6 7 8	syl3anc	⊢ ( 𝜑 → 0 ≤ ( Σ^ ‘ 𝐹 ) )