Metamath Proof Explorer


Theorem sge0gerpmpt

Description: The arbitrary sum of nonnegative extended reals is greater than or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0gerpmpt.xph xφ
sge0gerpmpt.a φAV
sge0gerpmpt.b φxAB0+∞
sge0gerpmpt.c φC*
sge0gerpmpt.rp φy+z𝒫AFinCsum^xzB+𝑒y
Assertion sge0gerpmpt φCsum^xAB

Proof

Step Hyp Ref Expression
1 sge0gerpmpt.xph xφ
2 sge0gerpmpt.a φAV
3 sge0gerpmpt.b φxAB0+∞
4 sge0gerpmpt.c φC*
5 sge0gerpmpt.rp φy+z𝒫AFinCsum^xzB+𝑒y
6 eqid xAB=xAB
7 1 3 6 fmptdf φxAB:A0+∞
8 elpwinss z𝒫AFinzA
9 8 resmptd z𝒫AFinxABz=xzB
10 9 eqcomd z𝒫AFinxzB=xABz
11 10 fveq2d z𝒫AFinsum^xzB=sum^xABz
12 11 oveq1d z𝒫AFinsum^xzB+𝑒y=sum^xABz+𝑒y
13 12 breq2d z𝒫AFinCsum^xzB+𝑒yCsum^xABz+𝑒y
14 13 biimpd z𝒫AFinCsum^xzB+𝑒yCsum^xABz+𝑒y
15 14 adantl φy+z𝒫AFinCsum^xzB+𝑒yCsum^xABz+𝑒y
16 15 reximdva φy+z𝒫AFinCsum^xzB+𝑒yz𝒫AFinCsum^xABz+𝑒y
17 5 16 mpd φy+z𝒫AFinCsum^xABz+𝑒y
18 2 7 4 17 sge0gerp φCsum^xAB