# Metamath Proof Explorer

## Theorem fsumge0

Description: If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumge0.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumge0.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
fsumge0.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
Assertion fsumge0 ${⊢}{\phi }\to 0\le \sum _{{k}\in {A}}{B}$

### Proof

Step Hyp Ref Expression
1 fsumge0.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fsumge0.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℝ$
3 fsumge0.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to 0\le {B}$
4 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
5 ax-resscn ${⊢}ℝ\subseteq ℂ$
6 4 5 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
7 6 a1i ${⊢}{\phi }\to \left[0,\mathrm{+\infty }\right)\subseteq ℂ$
8 ge0addcl ${⊢}\left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\to {x}+{y}\in \left[0,\mathrm{+\infty }\right)$
9 8 adantl ${⊢}\left({\phi }\wedge \left({x}\in \left[0,\mathrm{+\infty }\right)\wedge {y}\in \left[0,\mathrm{+\infty }\right)\right)\right)\to {x}+{y}\in \left[0,\mathrm{+\infty }\right)$
10 elrege0 ${⊢}{B}\in \left[0,\mathrm{+\infty }\right)↔\left({B}\in ℝ\wedge 0\le {B}\right)$
11 2 3 10 sylanbrc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right)$
12 0e0icopnf ${⊢}0\in \left[0,\mathrm{+\infty }\right)$
13 12 a1i ${⊢}{\phi }\to 0\in \left[0,\mathrm{+\infty }\right)$
14 7 9 1 11 13 fsumcllem ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}\in \left[0,\mathrm{+\infty }\right)$
15 elrege0 ${⊢}\sum _{{k}\in {A}}{B}\in \left[0,\mathrm{+\infty }\right)↔\left(\sum _{{k}\in {A}}{B}\in ℝ\wedge 0\le \sum _{{k}\in {A}}{B}\right)$
16 15 simprbi ${⊢}\sum _{{k}\in {A}}{B}\in \left[0,\mathrm{+\infty }\right)\to 0\le \sum _{{k}\in {A}}{B}$
17 14 16 syl ${⊢}{\phi }\to 0\le \sum _{{k}\in {A}}{B}$