Step |
Hyp |
Ref |
Expression |
1 |
|
monoordxr.p |
|- F/ k ph |
2 |
|
monoordxr.k |
|- F/_ k F |
3 |
|
monoordxr.n |
|- ( ph -> N e. ( ZZ>= ` M ) ) |
4 |
|
monoordxr.x |
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* ) |
5 |
|
monoordxr.l |
|- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) ) |
6 |
|
nfv |
|- F/ k j e. ( M ... N ) |
7 |
1 6
|
nfan |
|- F/ k ( ph /\ j e. ( M ... N ) ) |
8 |
|
nfcv |
|- F/_ k j |
9 |
2 8
|
nffv |
|- F/_ k ( F ` j ) |
10 |
|
nfcv |
|- F/_ k RR* |
11 |
9 10
|
nfel |
|- F/ k ( F ` j ) e. RR* |
12 |
7 11
|
nfim |
|- F/ k ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR* ) |
13 |
|
eleq1w |
|- ( k = j -> ( k e. ( M ... N ) <-> j e. ( M ... N ) ) ) |
14 |
13
|
anbi2d |
|- ( k = j -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ j e. ( M ... N ) ) ) ) |
15 |
|
fveq2 |
|- ( k = j -> ( F ` k ) = ( F ` j ) ) |
16 |
15
|
eleq1d |
|- ( k = j -> ( ( F ` k ) e. RR* <-> ( F ` j ) e. RR* ) ) |
17 |
14 16
|
imbi12d |
|- ( k = j -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* ) <-> ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR* ) ) ) |
18 |
12 17 4
|
chvarfv |
|- ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR* ) |
19 |
|
nfv |
|- F/ k j e. ( M ... ( N - 1 ) ) |
20 |
1 19
|
nfan |
|- F/ k ( ph /\ j e. ( M ... ( N - 1 ) ) ) |
21 |
|
nfcv |
|- F/_ k <_ |
22 |
|
nfcv |
|- F/_ k ( j + 1 ) |
23 |
2 22
|
nffv |
|- F/_ k ( F ` ( j + 1 ) ) |
24 |
9 21 23
|
nfbr |
|- F/ k ( F ` j ) <_ ( F ` ( j + 1 ) ) |
25 |
20 24
|
nfim |
|- F/ k ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` j ) <_ ( F ` ( j + 1 ) ) ) |
26 |
|
eleq1w |
|- ( k = j -> ( k e. ( M ... ( N - 1 ) ) <-> j e. ( M ... ( N - 1 ) ) ) ) |
27 |
26
|
anbi2d |
|- ( k = j -> ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) <-> ( ph /\ j e. ( M ... ( N - 1 ) ) ) ) ) |
28 |
|
fvoveq1 |
|- ( k = j -> ( F ` ( k + 1 ) ) = ( F ` ( j + 1 ) ) ) |
29 |
15 28
|
breq12d |
|- ( k = j -> ( ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> ( F ` j ) <_ ( F ` ( j + 1 ) ) ) ) |
30 |
27 29
|
imbi12d |
|- ( k = j -> ( ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) ) <-> ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` j ) <_ ( F ` ( j + 1 ) ) ) ) ) |
31 |
25 30 5
|
chvarfv |
|- ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` j ) <_ ( F ` ( j + 1 ) ) ) |
32 |
3 18 31
|
monoordxrv |
|- ( ph -> ( F ` M ) <_ ( F ` N ) ) |