Description: The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0nemnf.1 | ||
sge0nemnf.2 | |||
Assertion | sge0nemnf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0nemnf.1 | ||
2 | sge0nemnf.2 | ||
3 | 1 2 | sge0cl | |
4 | xrge0neqmnf | ||
5 | 3 4 | syl |