Theorem fsumge0cl

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

	Ref	Expression
Hypotheses	fsumge0cl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumge0cl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion	fsumge0cl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		fsumge0cl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fsumge0cl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3		0xr	⊢ 0 ∈ ℝ*
4	3	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
5		pnfxr	⊢ +∞ ∈ ℝ*
6	5	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
7		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
8	7 2	sselid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
9	1 8	fsumrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
10	9	rexrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
11	3	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ℝ* )
12	5	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → +∞ ∈ ℝ* )
13		icogelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
14	11 12 2 13	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
15	1 8 14	fsumge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
16	9	ltpnfd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < +∞ )
17	4 6 10 15 16	elicod	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) )