Theorem sge0ge0

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

	Ref	Expression
Hypotheses	sge0ge0.x	|- ( ph -> X e. V )
	sge0ge0.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion	sge0ge0	|- ( ph -> 0 <_ ( sum^ ` F ) )

Proof

Step	Hyp	Ref	Expression
1		sge0ge0.x	|- ( ph -> X e. V )
2		sge0ge0.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
3		0xr	|- 0 e. RR*
4	3	a1i	|- ( ph -> 0 e. RR* )
5		pnfxr	|- +oo e. RR*
6	5	a1i	|- ( ph -> +oo e. RR* )
7	1 2	sge0cl	|- ( ph -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
8		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ ( sum^ ` F ) e. ( 0 [,] +oo ) ) -> 0 <_ ( sum^ ` F ) )
9	4 6 7 8	syl3anc	|- ( ph -> 0 <_ ( sum^ ` F ) )