This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )