This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem monoord2xr

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

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

Proof

Step Hyp Ref Expression
1 monoord2xr.p 
 |-  F/ k ph
2 monoord2xr.k 
 |-  F/_ k F
3 monoord2xr.n 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 monoord2xr.x 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* )
5 monoord2xr.l 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
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 ( j + 1 )
22 2 21 nffv 
 |-  F/_ k ( F ` ( j + 1 ) )
23 nfcv 
 |-  F/_ k <_
24 22 23 9 nfbr 
 |-  F/ k ( F ` ( j + 1 ) ) <_ ( F ` j )
25 20 24 nfim 
 |-  F/ k ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) )
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 28 15 breq12d 
 |-  ( k = j -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> ( F ` ( j + 1 ) ) <_ ( F ` j ) ) )
30 27 29 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) ) <-> ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) ) ) )
31 25 30 5 chvarfv 
 |-  ( ( ph /\ j e. ( M ... ( N - 1 ) ) ) -> ( F ` ( j + 1 ) ) <_ ( F ` j ) )
32 3 18 31 monoord2xrv 
 |-  ( ph -> ( F ` N ) <_ ( F ` M ) )