Metamath Proof Explorer


Theorem monoordxr

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022)

Ref Expression
Hypotheses monoordxr.p
|- F/ k ph
monoordxr.k
|- F/_ k F
monoordxr.n
|- ( ph -> N e. ( ZZ>= ` M ) )
monoordxr.x
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* )
monoordxr.l
|- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
Assertion monoordxr
|- ( ph -> ( F ` M ) <_ ( F ` N ) )

Proof

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