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 
|- F/ k ph
sge0gtfsumgt.a 
|- ( ph -> A e. V )
sge0gtfsumgt.b 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )
sge0gtfsumgt.c 
|- ( ph -> C e. RR )
sge0gtfsumgt.l 
|- ( ph -> C < ( sum^ ` ( k e. A |-> B ) ) )
Assertion sge0gtfsumgt 
|- ( ph -> E. y e. ( ~P A i^i Fin ) C < sum_ k e. y B )

Proof

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