Metamath Proof Explorer


Theorem sge0nemnf

Description: The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0nemnf.1 φ A V
sge0nemnf.2 φ F : A 0 +∞
Assertion sge0nemnf φ sum^ F −∞

Proof

Step Hyp Ref Expression
1 sge0nemnf.1 φ A V
2 sge0nemnf.2 φ F : A 0 +∞
3 1 2 sge0cl φ sum^ F 0 +∞
4 xrge0neqmnf sum^ F 0 +∞ sum^ F −∞
5 3 4 syl φ sum^ F −∞