Metamath Proof Explorer


Theorem sge0lefi

Description: A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0lefi.1 φXV
sge0lefi.2 φF:X0+∞
sge0lefi.3 φA*
Assertion sge0lefi φsum^FAx𝒫XFinsum^FxA

Proof

Step Hyp Ref Expression
1 sge0lefi.1 φXV
2 sge0lefi.2 φF:X0+∞
3 sge0lefi.3 φA*
4 simpr φx𝒫XFinx𝒫XFin
5 2 adantr φx𝒫XFinF:X0+∞
6 elpwinss x𝒫XFinxX
7 6 adantl φx𝒫XFinxX
8 5 7 fssresd φx𝒫XFinFx:x0+∞
9 4 8 sge0xrcl φx𝒫XFinsum^Fx*
10 9 adantlr φsum^FAx𝒫XFinsum^Fx*
11 1 2 sge0xrcl φsum^F*
12 11 ad2antrr φsum^FAx𝒫XFinsum^F*
13 3 ad2antrr φsum^FAx𝒫XFinA*
14 1 adantr φx𝒫XFinXV
15 14 5 sge0less φx𝒫XFinsum^Fxsum^F
16 15 adantlr φsum^FAx𝒫XFinsum^Fxsum^F
17 simplr φsum^FAx𝒫XFinsum^FA
18 10 12 13 16 17 xrletrd φsum^FAx𝒫XFinsum^FxA
19 18 ralrimiva φsum^FAx𝒫XFinsum^FxA
20 19 ex φsum^FAx𝒫XFinsum^FxA
21 1 2 sge0sup φsum^F=supranx𝒫XFinsum^Fx*<
22 21 adantr φx𝒫XFinsum^FxAsum^F=supranx𝒫XFinsum^Fx*<
23 vex yV
24 eqid x𝒫XFinsum^Fx=x𝒫XFinsum^Fx
25 24 elrnmpt yVyranx𝒫XFinsum^Fxx𝒫XFiny=sum^Fx
26 23 25 ax-mp yranx𝒫XFinsum^Fxx𝒫XFiny=sum^Fx
27 26 biimpi yranx𝒫XFinsum^Fxx𝒫XFiny=sum^Fx
28 27 adantl φx𝒫XFinsum^FxAyranx𝒫XFinsum^Fxx𝒫XFiny=sum^Fx
29 nfv xφ
30 nfra1 xx𝒫XFinsum^FxA
31 29 30 nfan xφx𝒫XFinsum^FxA
32 nfcv _xy
33 nfmpt1 _xx𝒫XFinsum^Fx
34 33 nfrn _xranx𝒫XFinsum^Fx
35 32 34 nfel xyranx𝒫XFinsum^Fx
36 31 35 nfan xφx𝒫XFinsum^FxAyranx𝒫XFinsum^Fx
37 nfv xyA
38 simp3 x𝒫XFinsum^FxAx𝒫XFiny=sum^Fxy=sum^Fx
39 rspa x𝒫XFinsum^FxAx𝒫XFinsum^FxA
40 39 3adant3 x𝒫XFinsum^FxAx𝒫XFiny=sum^Fxsum^FxA
41 38 40 eqbrtrd x𝒫XFinsum^FxAx𝒫XFiny=sum^FxyA
42 41 3adant1l φx𝒫XFinsum^FxAx𝒫XFiny=sum^FxyA
43 42 3exp φx𝒫XFinsum^FxAx𝒫XFiny=sum^FxyA
44 43 adantr φx𝒫XFinsum^FxAyranx𝒫XFinsum^Fxx𝒫XFiny=sum^FxyA
45 36 37 44 rexlimd φx𝒫XFinsum^FxAyranx𝒫XFinsum^Fxx𝒫XFiny=sum^FxyA
46 28 45 mpd φx𝒫XFinsum^FxAyranx𝒫XFinsum^FxyA
47 46 ralrimiva φx𝒫XFinsum^FxAyranx𝒫XFinsum^FxyA
48 9 ralrimiva φx𝒫XFinsum^Fx*
49 24 rnmptss x𝒫XFinsum^Fx*ranx𝒫XFinsum^Fx*
50 48 49 syl φranx𝒫XFinsum^Fx*
51 50 adantr φx𝒫XFinsum^FxAranx𝒫XFinsum^Fx*
52 3 adantr φx𝒫XFinsum^FxAA*
53 supxrleub ranx𝒫XFinsum^Fx*A*supranx𝒫XFinsum^Fx*<Ayranx𝒫XFinsum^FxyA
54 51 52 53 syl2anc φx𝒫XFinsum^FxAsupranx𝒫XFinsum^Fx*<Ayranx𝒫XFinsum^FxyA
55 47 54 mpbird φx𝒫XFinsum^FxAsupranx𝒫XFinsum^Fx*<A
56 22 55 eqbrtrd φx𝒫XFinsum^FxAsum^FA
57 56 ex φx𝒫XFinsum^FxAsum^FA
58 20 57 impbid φsum^FAx𝒫XFinsum^FxA