Metamath Proof Explorer


Theorem sge0ltfirp

Description: If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ltfirp.x φ X V
sge0ltfirp.f φ F : X 0 +∞
sge0ltfirp.y φ Y +
sge0ltfirp.re φ sum^ F
Assertion sge0ltfirp φ x 𝒫 X Fin sum^ F < sum^ F x + Y

Proof

Step Hyp Ref Expression
1 sge0ltfirp.x φ X V
2 sge0ltfirp.f φ F : X 0 +∞
3 sge0ltfirp.y φ Y +
4 sge0ltfirp.re φ sum^ F
5 1 2 4 sge0rern φ ¬ +∞ ran F
6 2 5 fge0iccico φ F : X 0 +∞
7 6 sge0rnre φ ran x 𝒫 X Fin y x F y
8 sge0rnn0 ran x 𝒫 X Fin y x F y
9 8 a1i φ ran x 𝒫 X Fin y x F y
10 1 2 4 sge0rnbnd φ z w ran x 𝒫 X Fin y x F y w z
11 7 9 10 3 suprltrp φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w
12 nfv w φ
13 nfv w x 𝒫 X Fin sum^ F < sum^ F x + Y
14 simp1 φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w φ
15 vex w V
16 eqid x 𝒫 X Fin y x F y = x 𝒫 X Fin y x F y
17 16 elrnmpt w V w ran x 𝒫 X Fin y x F y x 𝒫 X Fin w = y x F y
18 15 17 ax-mp w ran x 𝒫 X Fin y x F y x 𝒫 X Fin w = y x F y
19 18 biimpi w ran x 𝒫 X Fin y x F y x 𝒫 X Fin w = y x F y
20 19 adantr w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin w = y x F y
21 nfmpt1 _ x x 𝒫 X Fin y x F y
22 21 nfrn _ x ran x 𝒫 X Fin y x F y
23 nfcv _ x
24 nfcv _ x <
25 22 23 24 nfsup _ x sup ran x 𝒫 X Fin y x F y <
26 nfcv _ x
27 nfcv _ x Y
28 25 26 27 nfov _ x sup ran x 𝒫 X Fin y x F y < Y
29 nfcv _ x w
30 28 24 29 nfbr x sup ran x 𝒫 X Fin y x F y < Y < w
31 simpl sup ran x 𝒫 X Fin y x F y < Y < w w = y x F y sup ran x 𝒫 X Fin y x F y < Y < w
32 simpr sup ran x 𝒫 X Fin y x F y < Y < w w = y x F y w = y x F y
33 31 32 breqtrd sup ran x 𝒫 X Fin y x F y < Y < w w = y x F y sup ran x 𝒫 X Fin y x F y < Y < y x F y
34 33 ex sup ran x 𝒫 X Fin y x F y < Y < w w = y x F y sup ran x 𝒫 X Fin y x F y < Y < y x F y
35 34 a1d sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin w = y x F y sup ran x 𝒫 X Fin y x F y < Y < y x F y
36 30 35 reximdai sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin w = y x F y x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y
37 36 adantl w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin w = y x F y x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y
38 20 37 mpd w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y
39 38 3adant1 φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y
40 simpl φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y φ x 𝒫 X Fin
41 1 2 4 sge0supre φ sum^ F = sup ran x 𝒫 X Fin y x F y <
42 41 oveq1d φ sum^ F Y = sup ran x 𝒫 X Fin y x F y < Y
43 42 adantr φ sup ran x 𝒫 X Fin y x F y < Y < y x F y sum^ F Y = sup ran x 𝒫 X Fin y x F y < Y
44 simpr φ sup ran x 𝒫 X Fin y x F y < Y < y x F y sup ran x 𝒫 X Fin y x F y < Y < y x F y
45 43 44 eqbrtrd φ sup ran x 𝒫 X Fin y x F y < Y < y x F y sum^ F Y < y x F y
46 45 adantlr φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y sum^ F Y < y x F y
47 simpr φ x 𝒫 X Fin sum^ F Y < y x F y sum^ F Y < y x F y
48 4 adantr φ x 𝒫 X Fin sum^ F
49 3 rpred φ Y
50 49 adantr φ x 𝒫 X Fin Y
51 elinel2 x 𝒫 X Fin x Fin
52 51 adantl φ x 𝒫 X Fin x Fin
53 rge0ssre 0 +∞
54 6 adantr φ x 𝒫 X Fin F : X 0 +∞
55 54 adantr φ x 𝒫 X Fin y x F : X 0 +∞
56 elpwinss x 𝒫 X Fin x X
57 56 adantl φ x 𝒫 X Fin x X
58 57 sselda φ x 𝒫 X Fin y x y X
59 55 58 ffvelrnd φ x 𝒫 X Fin y x F y 0 +∞
60 53 59 sselid φ x 𝒫 X Fin y x F y
61 52 60 fsumrecl φ x 𝒫 X Fin y x F y
62 48 50 61 ltsubaddd φ x 𝒫 X Fin sum^ F Y < y x F y sum^ F < y x F y + Y
63 62 adantr φ x 𝒫 X Fin sum^ F Y < y x F y sum^ F Y < y x F y sum^ F < y x F y + Y
64 47 63 mpbid φ x 𝒫 X Fin sum^ F Y < y x F y sum^ F < y x F y + Y
65 54 57 fssresd φ x 𝒫 X Fin F x : x 0 +∞
66 52 65 sge0fsum φ x 𝒫 X Fin sum^ F x = y x F x y
67 fvres y x F x y = F y
68 67 sumeq2i y x F x y = y x F y
69 68 a1i φ x 𝒫 X Fin y x F x y = y x F y
70 66 69 eqtr2d φ x 𝒫 X Fin y x F y = sum^ F x
71 70 oveq1d φ x 𝒫 X Fin y x F y + Y = sum^ F x + Y
72 71 adantr φ x 𝒫 X Fin sum^ F Y < y x F y y x F y + Y = sum^ F x + Y
73 64 72 breqtrd φ x 𝒫 X Fin sum^ F Y < y x F y sum^ F < sum^ F x + Y
74 40 46 73 syl2anc φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y sum^ F < sum^ F x + Y
75 74 ex φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y sum^ F < sum^ F x + Y
76 75 reximdva φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y x 𝒫 X Fin sum^ F < sum^ F x + Y
77 76 imp φ x 𝒫 X Fin sup ran x 𝒫 X Fin y x F y < Y < y x F y x 𝒫 X Fin sum^ F < sum^ F x + Y
78 14 39 77 syl2anc φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin sum^ F < sum^ F x + Y
79 78 3exp φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin sum^ F < sum^ F x + Y
80 12 13 79 rexlimd φ w ran x 𝒫 X Fin y x F y sup ran x 𝒫 X Fin y x F y < Y < w x 𝒫 X Fin sum^ F < sum^ F x + Y
81 11 80 mpd φ x 𝒫 X Fin sum^ F < sum^ F x + Y