Metamath Proof Explorer


Theorem sge0ge0

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

Ref Expression
Hypotheses sge0ge0.x φXV
sge0ge0.f φF:X0+∞
Assertion sge0ge0 φ0sum^F

Proof

Step Hyp Ref Expression
1 sge0ge0.x φXV
2 sge0ge0.f φF:X0+∞
3 0xr 0*
4 3 a1i φ0*
5 pnfxr +∞*
6 5 a1i φ+∞*
7 1 2 sge0cl φsum^F0+∞
8 iccgelb 0*+∞*sum^F0+∞0sum^F
9 4 6 7 8 syl3anc φ0sum^F