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	$$⊢\phi \to A\in V$$
	sge0nemnf.2	$$⊢\phi \to F:A⟶\left[0,\mathrm{+\infty }\right]$$
Assertion	sge0nemnf	$$⊢\phi \to \mathrm{sum^}\left(F\right)\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		sge0nemnf.1	$$⊢\phi \to A\in V$$
2		sge0nemnf.2	$$⊢\phi \to F:A⟶\left[0,\mathrm{+\infty }\right]$$
3	1 2	sge0cl	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right]$$
4		xrge0neqmnf	$$⊢\mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right]\to \mathrm{sum^}\left(F\right)\ne \mathrm{-\infty }$$
5	3 4	syl	$$⊢\phi \to \mathrm{sum^}\left(F\right)\ne \mathrm{-\infty }$$