Metamath Proof Explorer


Theorem sge0ltfirpmpt

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 xφ
sge0ltfirpmpt.a φAV
sge0ltfirpmpt.b φxAB0+∞
sge0ltfirpmpt.rp φY+
sge0ltfirpmpt.re φsum^xAB
Assertion sge0ltfirpmpt φy𝒫AFinsum^xAB<sum^xyB+Y

Proof

Step Hyp Ref Expression
1 sge0ltfirpmpt.xph xφ
2 sge0ltfirpmpt.a φAV
3 sge0ltfirpmpt.b φxAB0+∞
4 sge0ltfirpmpt.rp φY+
5 sge0ltfirpmpt.re φsum^xAB
6 eqid xAB=xAB
7 1 3 6 fmptdf φxAB:A0+∞
8 2 7 4 5 sge0ltfirp φy𝒫AFinsum^xAB<sum^xABy+Y
9 simpr y𝒫AFinsum^xAB<sum^xABy+Ysum^xAB<sum^xABy+Y
10 elpwinss y𝒫AFinyA
11 10 resmptd y𝒫AFinxABy=xyB
12 11 fveq2d y𝒫AFinsum^xABy=sum^xyB
13 12 oveq1d y𝒫AFinsum^xABy+Y=sum^xyB+Y
14 13 adantr y𝒫AFinsum^xAB<sum^xABy+Ysum^xABy+Y=sum^xyB+Y
15 9 14 breqtrd y𝒫AFinsum^xAB<sum^xABy+Ysum^xAB<sum^xyB+Y
16 15 ex y𝒫AFinsum^xAB<sum^xABy+Ysum^xAB<sum^xyB+Y
17 16 reximia y𝒫AFinsum^xAB<sum^xABy+Yy𝒫AFinsum^xAB<sum^xyB+Y
18 17 a1i φy𝒫AFinsum^xAB<sum^xABy+Yy𝒫AFinsum^xAB<sum^xyB+Y
19 8 18 mpd φy𝒫AFinsum^xAB<sum^xyB+Y