Description: If the extended sum of nonnegative reals is not +oo , then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0ltfirpmpt.xph | |
|
sge0ltfirpmpt.a | |
||
sge0ltfirpmpt.b | |
||
sge0ltfirpmpt.rp | |
||
sge0ltfirpmpt.re | |
||
Assertion | sge0ltfirpmpt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0ltfirpmpt.xph | |
|
2 | sge0ltfirpmpt.a | |
|
3 | sge0ltfirpmpt.b | |
|
4 | sge0ltfirpmpt.rp | |
|
5 | sge0ltfirpmpt.re | |
|
6 | eqid | |
|
7 | 1 3 6 | fmptdf | |
8 | 2 7 4 5 | sge0ltfirp | |
9 | simpr | |
|
10 | elpwinss | |
|
11 | 10 | resmptd | |
12 | 11 | fveq2d | |
13 | 12 | oveq1d | |
14 | 13 | adantr | |
15 | 9 14 | breqtrd | |
16 | 15 | ex | |
17 | 16 | reximia | |
18 | 17 | a1i | |
19 | 8 18 | mpd | |