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 φAFin
fsumge0cl.b φkAB0+∞
Assertion fsumge0cl φkAB0+∞

Proof

Step Hyp Ref Expression
1 fsumge0cl.a φAFin
2 fsumge0cl.b φkAB0+∞
3 0xr 0*
4 3 a1i φ0*
5 pnfxr +∞*
6 5 a1i φ+∞*
7 rge0ssre 0+∞
8 7 2 sselid φkAB
9 1 8 fsumrecl φkAB
10 9 rexrd φkAB*
11 3 a1i φkA0*
12 5 a1i φkA+∞*
13 icogelb 0*+∞*B0+∞0B
14 11 12 2 13 syl3anc φkA0B
15 1 8 14 fsumge0 φ0kAB
16 9 ltpnfd φkAB<+∞
17 4 6 10 15 16 elicod φkAB0+∞