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