Description: The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsumge0cl.a | |
|
fsumge0cl.b | |
||
Assertion | fsumge0cl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsumge0cl.a | |
|
2 | fsumge0cl.b | |
|
3 | 0xr | |
|
4 | 3 | a1i | |
5 | pnfxr | |
|
6 | 5 | a1i | |
7 | rge0ssre | |
|
8 | 7 2 | sselid | |
9 | 1 8 | fsumrecl | |
10 | 9 | rexrd | |
11 | 3 | a1i | |
12 | 5 | a1i | |
13 | icogelb | |
|
14 | 11 12 2 13 | syl3anc | |
15 | 1 8 14 | fsumge0 | |
16 | 9 | ltpnfd | |
17 | 4 6 10 15 16 | elicod | |