Description: If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0ssrempt.xph | |
|
sge0ssrempt.a | |
||
sge0ssrempt.b | |
||
sge0ssrempt.re | |
||
sge0ssrempt.c | |
||
Assertion | sge0ssrempt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0ssrempt.xph | |
|
2 | sge0ssrempt.a | |
|
3 | sge0ssrempt.b | |
|
4 | sge0ssrempt.re | |
|
5 | sge0ssrempt.c | |
|
6 | 5 | resmptd | |
7 | 6 | fveq2d | |
8 | 7 | eqcomd | |
9 | eqid | |
|
10 | 1 3 9 | fmptdf | |
11 | 2 10 4 | sge0ssre | |
12 | 8 11 | eqeltrd | |