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	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumge0cl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right)$$
Assertion	fsumge0cl	$$⊢\phi \to \sum _{k\in A}B\in \left[0,\mathrm{+\infty }\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsumge0cl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fsumge0cl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right)$$
3		0xr	$$⊢0\in {ℝ}^{*}$$
4	3	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
5		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
6	5	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
7		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
8	7 2	sselid	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
9	1 8	fsumrecl	$$⊢\phi \to \sum _{k\in A}B\in ℝ$$
10	9	rexrd	$$⊢\phi \to \sum _{k\in A}B\in {ℝ}^{*}$$
11	3	a1i	$$⊢\left(\phi \wedge k\in A\right)\to 0\in {ℝ}^{*}$$
12	5	a1i	$$⊢\left(\phi \wedge k\in A\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
13		icogelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge B\in \left[0,\mathrm{+\infty }\right)\right)\to 0\le B$$
14	11 12 2 13	syl3anc	$$⊢\left(\phi \wedge k\in A\right)\to 0\le B$$
15	1 8 14	fsumge0	$$⊢\phi \to 0\le \sum _{k\in A}B$$
16	9	ltpnfd	$$⊢\phi \to \sum _{k\in A}B<\mathrm{+\infty }$$
17	4 6 10 15 16	elicod	$$⊢\phi \to \sum _{k\in A}B\in \left[0,\mathrm{+\infty }\right)$$