Step |
Hyp |
Ref |
Expression |
1 |
|
xlimmnfmpt.k |
|- F/ k ph |
2 |
|
xlimmnfmpt.m |
|- ( ph -> M e. ZZ ) |
3 |
|
xlimmnfmpt.z |
|- Z = ( ZZ>= ` M ) |
4 |
|
xlimmnfmpt.b |
|- ( ( ph /\ k e. Z ) -> B e. RR* ) |
5 |
|
xlimmnfmpt.f |
|- F = ( k e. Z |-> B ) |
6 |
|
nfmpt1 |
|- F/_ k ( k e. Z |-> B ) |
7 |
5 6
|
nfcxfr |
|- F/_ k F |
8 |
1 4 5
|
fmptdf |
|- ( ph -> F : Z --> RR* ) |
9 |
7 2 3 8
|
xlimmnf |
|- ( ph -> ( F ~~>* -oo <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y ) ) |
10 |
|
nfv |
|- F/ k i e. Z |
11 |
1 10
|
nfan |
|- F/ k ( ph /\ i e. Z ) |
12 |
3
|
uztrn2 |
|- ( ( i e. Z /\ k e. ( ZZ>= ` i ) ) -> k e. Z ) |
13 |
12
|
adantll |
|- ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> k e. Z ) |
14 |
|
simpll |
|- ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ph ) |
15 |
14 13 4
|
syl2anc |
|- ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> B e. RR* ) |
16 |
5
|
fvmpt2 |
|- ( ( k e. Z /\ B e. RR* ) -> ( F ` k ) = B ) |
17 |
13 15 16
|
syl2anc |
|- ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( F ` k ) = B ) |
18 |
17
|
breq1d |
|- ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( F ` k ) <_ y <-> B <_ y ) ) |
19 |
11 18
|
ralbida |
|- ( ( ph /\ i e. Z ) -> ( A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> A. k e. ( ZZ>= ` i ) B <_ y ) ) |
20 |
19
|
rexbidva |
|- ( ph -> ( E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y ) ) |
21 |
20
|
ralbidv |
|- ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y ) ) |
22 |
|
breq2 |
|- ( y = x -> ( B <_ y <-> B <_ x ) ) |
23 |
22
|
rexralbidv |
|- ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> E. i e. Z A. k e. ( ZZ>= ` i ) B <_ x ) ) |
24 |
|
fveq2 |
|- ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) ) |
25 |
24
|
raleqdv |
|- ( i = j -> ( A. k e. ( ZZ>= ` i ) B <_ x <-> A. k e. ( ZZ>= ` j ) B <_ x ) ) |
26 |
25
|
cbvrexvw |
|- ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) |
27 |
23 26
|
syl6bb |
|- ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) ) |
28 |
27
|
cbvralvw |
|- ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) |
29 |
28
|
a1i |
|- ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) ) |
30 |
9 21 29
|
3bitrd |
|- ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) ) |