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	|- ( ph -> A e. V )
	sge0nemnf.2	|- ( ph -> F : A --> ( 0 [,] +oo ) )
Assertion	sge0nemnf	|- ( ph -> ( sum^ ` F ) =/= -oo )

Proof

Step	Hyp	Ref	Expression
1		sge0nemnf.1	|- ( ph -> A e. V )
2		sge0nemnf.2	|- ( ph -> F : A --> ( 0 [,] +oo ) )
3	1 2	sge0cl	|- ( ph -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
4		xrge0neqmnf	|- ( ( sum^ ` F ) e. ( 0 [,] +oo ) -> ( sum^ ` F ) =/= -oo )
5	3 4	syl	|- ( ph -> ( sum^ ` F ) =/= -oo )