Theorem sge0ge0

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

	Ref	Expression
Hypotheses	sge0ge0.x	$$⊢\phi \to X\in V$$
	sge0ge0.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
Assertion	sge0ge0	$$⊢\phi \to 0\le \mathrm{sum^}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0ge0.x	$$⊢\phi \to X\in V$$
2		sge0ge0.f	$$⊢\phi \to F:X⟶\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	1 2	sge0cl	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right]$$
8		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge \mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le \mathrm{sum^}\left(F\right)$$
9	4 6 7 8	syl3anc	$$⊢\phi \to 0\le \mathrm{sum^}\left(F\right)$$