Metamath Proof Explorer


Theorem sge0gtfsumgt

Description: If the generalized sum of nonnegative reals is larger than a given number, then that number can be dominated by a finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0gtfsumgt.k k φ
sge0gtfsumgt.a φ A V
sge0gtfsumgt.b φ k A B 0 +∞
sge0gtfsumgt.c φ C
sge0gtfsumgt.l φ C < sum^ k A B
Assertion sge0gtfsumgt φ y 𝒫 A Fin C < k y B

Proof

Step Hyp Ref Expression
1 sge0gtfsumgt.k k φ
2 sge0gtfsumgt.a φ A V
3 sge0gtfsumgt.b φ k A B 0 +∞
4 sge0gtfsumgt.c φ C
5 sge0gtfsumgt.l φ C < sum^ k A B
6 nfcv _ k sum^
7 nfmpt1 _ k k A B
8 6 7 nffv _ k sum^ k A B
9 nfcv _ k
10 8 9 nfel k sum^ k A B
11 1 10 nfan k φ sum^ k A B
12 2 adantr φ sum^ k A B A V
13 icossicc 0 +∞ 0 +∞
14 13 3 sseldi φ k A B 0 +∞
15 14 adantlr φ sum^ k A B k A B 0 +∞
16 5 adantr φ sum^ k A B C < sum^ k A B
17 4 adantr φ sum^ k A B C
18 simpr φ sum^ k A B sum^ k A B
19 difrp C sum^ k A B C < sum^ k A B sum^ k A B C +
20 17 18 19 syl2anc φ sum^ k A B C < sum^ k A B sum^ k A B C +
21 16 20 mpbid φ sum^ k A B sum^ k A B C +
22 11 12 15 21 18 sge0ltfirpmpt2 φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C
23 simpr φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B < k y B + sum^ k A B - C
24 nfv k y 𝒫 A Fin
25 1 24 nfan k φ y 𝒫 A Fin
26 elinel2 y 𝒫 A Fin y Fin
27 26 adantl φ y 𝒫 A Fin y Fin
28 simpll φ y 𝒫 A Fin k y φ
29 elpwinss y 𝒫 A Fin y A
30 29 adantr y 𝒫 A Fin k y y A
31 simpr y 𝒫 A Fin k y k y
32 30 31 sseldd y 𝒫 A Fin k y k A
33 32 adantll φ y 𝒫 A Fin k y k A
34 rge0ssre 0 +∞
35 34 3 sseldi φ k A B
36 28 33 35 syl2anc φ y 𝒫 A Fin k y B
37 25 27 36 fsumreclf φ y 𝒫 A Fin k y B
38 37 recnd φ y 𝒫 A Fin k y B
39 38 ad4ant13 φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C k y B
40 18 ad2antrr φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B
41 40 recnd φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B
42 17 ad2antrr φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C C
43 42 recnd φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C C
44 41 43 subcld φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B C
45 39 44 addcomd φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C k y B + sum^ k A B - C = sum^ k A B - C + k y B
46 23 45 breqtrd φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B < sum^ k A B - C + k y B
47 40 42 resubcld φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B C
48 37 ad4ant13 φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C k y B
49 40 47 48 ltsubadd2d φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B sum^ k A B C < k y B sum^ k A B < sum^ k A B - C + k y B
50 46 49 mpbird φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B sum^ k A B C < k y B
51 41 43 nncand φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B sum^ k A B C = C
52 51 breq1d φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C sum^ k A B sum^ k A B C < k y B C < k y B
53 50 52 mpbid φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C C < k y B
54 53 ex φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C C < k y B
55 54 reximdva φ sum^ k A B y 𝒫 A Fin sum^ k A B < k y B + sum^ k A B - C y 𝒫 A Fin C < k y B
56 22 55 mpd φ sum^ k A B y 𝒫 A Fin C < k y B
57 simpl φ ¬ sum^ k A B φ
58 simpr φ ¬ sum^ k A B ¬ sum^ k A B
59 eqid k A B = k A B
60 1 3 59 fmptdf φ k A B : A 0 +∞
61 13 a1i φ 0 +∞ 0 +∞
62 60 61 fssd φ k A B : A 0 +∞
63 2 62 sge0repnf φ sum^ k A B ¬ sum^ k A B = +∞
64 63 adantr φ ¬ sum^ k A B sum^ k A B ¬ sum^ k A B = +∞
65 58 64 mtbid φ ¬ sum^ k A B ¬ ¬ sum^ k A B = +∞
66 notnotb sum^ k A B = +∞ ¬ ¬ sum^ k A B = +∞
67 65 66 sylibr φ ¬ sum^ k A B sum^ k A B = +∞
68 8 nfeq1 k sum^ k A B = +∞
69 1 68 nfan k φ sum^ k A B = +∞
70 2 adantr φ sum^ k A B = +∞ A V
71 3 adantlr φ sum^ k A B = +∞ k A B 0 +∞
72 simpr φ sum^ k A B = +∞ sum^ k A B = +∞
73 4 adantr φ sum^ k A B = +∞ C
74 69 70 71 72 73 sge0pnffsumgt φ sum^ k A B = +∞ y 𝒫 A Fin C < k y B
75 57 67 74 syl2anc φ ¬ sum^ k A B y 𝒫 A Fin C < k y B
76 56 75 pm2.61dan φ y 𝒫 A Fin C < k y B