Metamath Proof Explorer

Theorem sge0uzfsumgt

Description: If a real number is smaller than a generalized sum of nonnegative reals, then it is smaller than some finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses sge0uzfsumgt.p 
|- F/ k ph
sge0uzfsumgt.h 
|- ( ph -> K e. ZZ )
sge0uzfsumgt.z 
|- Z = ( ZZ>= ` K )
sge0uzfsumgt.b 
|- ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )
sge0uzfsumgt.c 
|- ( ph -> C e. RR )
sge0uzfsumgt.l 
|- ( ph -> C < ( sum^ ` ( k e. Z |-> B ) ) )
Assertion sge0uzfsumgt 
|- ( ph -> E. m e. Z C < sum_ k e. ( K ... m ) B )

Proof

Step Hyp Ref Expression
1 sge0uzfsumgt.p 
 |-  F/ k ph
2 sge0uzfsumgt.h 
 |-  ( ph -> K e. ZZ )
3 sge0uzfsumgt.z 
 |-  Z = ( ZZ>= ` K )
4 sge0uzfsumgt.b 
 |-  ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )
5 sge0uzfsumgt.c 
 |-  ( ph -> C e. RR )
6 sge0uzfsumgt.l 
 |-  ( ph -> C < ( sum^ ` ( k e. Z |-> B ) ) )
7 3 fvexi 
 |-  Z e. _V
8 7 a1i 
 |-  ( ph -> Z e. _V )
9 1 8 4 5 6 sge0gtfsumgt 
 |-  ( ph -> E. x e. ( ~P Z i^i Fin ) C < sum_ k e. x B )
10 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> K e. ZZ )
11 elpwinss 
 |-  ( x e. ( ~P Z i^i Fin ) -> x C_ Z )
12 11 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> x C_ Z )
13 elinel2 
 |-  ( x e. ( ~P Z i^i Fin ) -> x e. Fin )
14 13 3ad2ant2 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> x e. Fin )
15 10 3 12 14 uzfissfz 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> E. m e. Z x C_ ( K ... m ) )
16 5 ad2antrr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> C e. RR )
17 nfv 
 |-  F/ k x C_ ( K ... m )
18 1 17 nfan 
 |-  F/ k ( ph /\ x C_ ( K ... m ) )
19 fzfid 
 |-  ( ( ph /\ x C_ ( K ... m ) ) -> ( K ... m ) e. Fin )
20 simpr 
 |-  ( ( ph /\ x C_ ( K ... m ) ) -> x C_ ( K ... m ) )
21 19 20 ssfid 
 |-  ( ( ph /\ x C_ ( K ... m ) ) -> x e. Fin )
22 simpll 
 |-  ( ( ( ph /\ x C_ ( K ... m ) ) /\ k e. x ) -> ph )
23 20 sselda 
 |-  ( ( ( ph /\ x C_ ( K ... m ) ) /\ k e. x ) -> k e. ( K ... m ) )
24 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
25 fzssuz 
 |-  ( K ... m ) C_ ( ZZ>= ` K )
26 25 3 sseqtrri 
 |-  ( K ... m ) C_ Z
27 id 
 |-  ( k e. ( K ... m ) -> k e. ( K ... m ) )
28 26 27 sseldi 
 |-  ( k e. ( K ... m ) -> k e. Z )
29 28 4 sylan2 
 |-  ( ( ph /\ k e. ( K ... m ) ) -> B e. ( 0 [,) +oo ) )
30 24 29 sseldi 
 |-  ( ( ph /\ k e. ( K ... m ) ) -> B e. RR )
31 22 23 30 syl2anc 
 |-  ( ( ( ph /\ x C_ ( K ... m ) ) /\ k e. x ) -> B e. RR )
32 18 21 31 fsumreclf 
 |-  ( ( ph /\ x C_ ( K ... m ) ) -> sum_ k e. x B e. RR )
33 32 adantlr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> sum_ k e. x B e. RR )
34 fzfid 
 |-  ( ph -> ( K ... m ) e. Fin )
35 1 34 30 fsumreclf 
 |-  ( ph -> sum_ k e. ( K ... m ) B e. RR )
36 35 ad2antrr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> sum_ k e. ( K ... m ) B e. RR )
37 simplr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> C < sum_ k e. x B )
38 30 adantlr 
 |-  ( ( ( ph /\ x C_ ( K ... m ) ) /\ k e. ( K ... m ) ) -> B e. RR )
39 0xr 
 |-  0 e. RR*
40 39 a1i 
 |-  ( ( ph /\ k e. ( K ... m ) ) -> 0 e. RR* )
41 pnfxr 
 |-  +oo e. RR*
42 41 a1i 
 |-  ( ( ph /\ k e. ( K ... m ) ) -> +oo e. RR* )
43 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,) +oo ) ) -> 0 <_ B )
44 40 42 29 43 syl3anc 
 |-  ( ( ph /\ k e. ( K ... m ) ) -> 0 <_ B )
45 44 adantlr 
 |-  ( ( ( ph /\ x C_ ( K ... m ) ) /\ k e. ( K ... m ) ) -> 0 <_ B )
46 18 19 38 45 20 fsumlessf 
 |-  ( ( ph /\ x C_ ( K ... m ) ) -> sum_ k e. x B <_ sum_ k e. ( K ... m ) B )
47 46 adantlr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> sum_ k e. x B <_ sum_ k e. ( K ... m ) B )
48 16 33 36 37 47 ltletrd 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ x C_ ( K ... m ) ) -> C < sum_ k e. ( K ... m ) B )
49 48 ex 
 |-  ( ( ph /\ C < sum_ k e. x B ) -> ( x C_ ( K ... m ) -> C < sum_ k e. ( K ... m ) B ) )
50 49 adantr 
 |-  ( ( ( ph /\ C < sum_ k e. x B ) /\ m e. Z ) -> ( x C_ ( K ... m ) -> C < sum_ k e. ( K ... m ) B ) )
51 50 3adantl2 
 |-  ( ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) /\ m e. Z ) -> ( x C_ ( K ... m ) -> C < sum_ k e. ( K ... m ) B ) )
52 51 reximdva 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> ( E. m e. Z x C_ ( K ... m ) -> E. m e. Z C < sum_ k e. ( K ... m ) B ) )
53 15 52 mpd 
 |-  ( ( ph /\ x e. ( ~P Z i^i Fin ) /\ C < sum_ k e. x B ) -> E. m e. Z C < sum_ k e. ( K ... m ) B )
54 53 3exp 
 |-  ( ph -> ( x e. ( ~P Z i^i Fin ) -> ( C < sum_ k e. x B -> E. m e. Z C < sum_ k e. ( K ... m ) B ) ) )
55 54 rexlimdv 
 |-  ( ph -> ( E. x e. ( ~P Z i^i Fin ) C < sum_ k e. x B -> E. m e. Z C < sum_ k e. ( K ... m ) B ) )
56 9 55 mpd 
 |-  ( ph -> E. m e. Z C < sum_ k e. ( K ... m ) B )