# Metamath Proof Explorer

## 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 sseldi
` |-  ( ( 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 ) )`