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 ) |