# Metamath Proof Explorer

## 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 sseldi ${⊢}\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)$