Theorem fsumge0cl

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

	Ref	Expression
Hypotheses	fsumge0cl.a	|- ( ph -> A e. Fin )
	fsumge0cl.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
Assertion	fsumge0cl	|- ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )

Proof

Step	Hyp	Ref	Expression
1		fsumge0cl.a	|- ( ph -> A e. Fin )
2		fsumge0cl.b	|- ( ( ph /\ k e. A ) -> B e. ( 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		rge0ssre	|- ( 0 [,) +oo ) C_ RR
8	7 2	sselid	|- ( ( ph /\ k e. A ) -> B e. RR )
9	1 8	fsumrecl	|- ( ph -> sum_ k e. A B e. RR )
10	9	rexrd	|- ( ph -> sum_ k e. A B e. RR* )
11	3	a1i	|- ( ( ph /\ k e. A ) -> 0 e. RR* )
12	5	a1i	|- ( ( ph /\ k e. A ) -> +oo e. RR* )
13		icogelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,) +oo ) ) -> 0 <_ B )
14	11 12 2 13	syl3anc	|- ( ( ph /\ k e. A ) -> 0 <_ B )
15	1 8 14	fsumge0	|- ( ph -> 0 <_ sum_ k e. A B )
16	9	ltpnfd	|- ( ph -> sum_ k e. A B < +oo )
17	4 6 10 15 16	elicod	|- ( ph -> sum_ k e. A B e. ( 0 [,) +oo ) )