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 sselid
 |-  ( k e. ( K ... m ) -> k e. Z )
29 28 4 sylan2
 |-  ( ( ph /\ k e. ( K ... m ) ) -> B e. ( 0 [,) +oo ) )
30 24 29 sselid
 |-  ( ( 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 )