Metamath Proof Explorer


Theorem monoord2xrv

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

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

Proof

Step Hyp Ref Expression
1 monoord2xrv.n
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 monoord2xrv.x
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* )
3 monoord2xrv.l
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
4 2 xnegcld
 |-  ( ( ph /\ k e. ( M ... N ) ) -> -e ( F ` k ) e. RR* )
5 4 fmpttd
 |-  ( ph -> ( k e. ( M ... N ) |-> -e ( F ` k ) ) : ( M ... N ) --> RR* )
6 5 ffvelrnda
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` n ) e. RR* )
7 3 ralrimiva
 |-  ( ph -> A. k e. ( M ... ( N - 1 ) ) ( F ` ( k + 1 ) ) <_ ( F ` k ) )
8 fvoveq1
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
9 fveq2
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
10 8 9 breq12d
 |-  ( k = n -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> ( F ` ( n + 1 ) ) <_ ( F ` n ) ) )
11 10 cbvralvw
 |-  ( A. k e. ( M ... ( N - 1 ) ) ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> A. n e. ( M ... ( N - 1 ) ) ( F ` ( n + 1 ) ) <_ ( F ` n ) )
12 7 11 sylib
 |-  ( ph -> A. n e. ( M ... ( N - 1 ) ) ( F ` ( n + 1 ) ) <_ ( F ` n ) )
13 12 r19.21bi
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` ( n + 1 ) ) <_ ( F ` n ) )
14 fzp1elp1
 |-  ( n e. ( M ... ( N - 1 ) ) -> ( n + 1 ) e. ( M ... ( ( N - 1 ) + 1 ) ) )
15 14 adantl
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( M ... ( ( N - 1 ) + 1 ) ) )
16 eluzelz
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
17 1 16 syl
 |-  ( ph -> N e. ZZ )
18 17 zcnd
 |-  ( ph -> N e. CC )
19 ax-1cn
 |-  1 e. CC
20 npcan
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
21 18 19 20 sylancl
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
22 21 oveq2d
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
23 22 adantr
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
24 15 23 eleqtrd
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( M ... N ) )
25 2 ralrimiva
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) e. RR* )
26 25 adantr
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> A. k e. ( M ... N ) ( F ` k ) e. RR* )
27 fveq2
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
28 27 eleq1d
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. RR* <-> ( F ` ( n + 1 ) ) e. RR* ) )
29 28 rspcv
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` ( n + 1 ) ) e. RR* ) )
30 24 26 29 sylc
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` ( n + 1 ) ) e. RR* )
31 fzssp1
 |-  ( M ... ( N - 1 ) ) C_ ( M ... ( ( N - 1 ) + 1 ) )
32 31 22 sseqtrid
 |-  ( ph -> ( M ... ( N - 1 ) ) C_ ( M ... N ) )
33 32 sselda
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ( M ... N ) )
34 9 eleq1d
 |-  ( k = n -> ( ( F ` k ) e. RR* <-> ( F ` n ) e. RR* ) )
35 34 rspcv
 |-  ( n e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` n ) e. RR* ) )
36 33 26 35 sylc
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` n ) e. RR* )
37 xleneg
 |-  ( ( ( F ` ( n + 1 ) ) e. RR* /\ ( F ` n ) e. RR* ) -> ( ( F ` ( n + 1 ) ) <_ ( F ` n ) <-> -e ( F ` n ) <_ -e ( F ` ( n + 1 ) ) ) )
38 30 36 37 syl2anc
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( F ` ( n + 1 ) ) <_ ( F ` n ) <-> -e ( F ` n ) <_ -e ( F ` ( n + 1 ) ) ) )
39 13 38 mpbid
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> -e ( F ` n ) <_ -e ( F ` ( n + 1 ) ) )
40 9 xnegeqd
 |-  ( k = n -> -e ( F ` k ) = -e ( F ` n ) )
41 eqid
 |-  ( k e. ( M ... N ) |-> -e ( F ` k ) ) = ( k e. ( M ... N ) |-> -e ( F ` k ) )
42 xnegex
 |-  -e ( F ` n ) e. _V
43 40 41 42 fvmpt
 |-  ( n e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` n ) = -e ( F ` n ) )
44 33 43 syl
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` n ) = -e ( F ` n ) )
45 27 xnegeqd
 |-  ( k = ( n + 1 ) -> -e ( F ` k ) = -e ( F ` ( n + 1 ) ) )
46 xnegex
 |-  -e ( F ` ( n + 1 ) ) e. _V
47 45 41 46 fvmpt
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` ( n + 1 ) ) = -e ( F ` ( n + 1 ) ) )
48 24 47 syl
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` ( n + 1 ) ) = -e ( F ` ( n + 1 ) ) )
49 39 44 48 3brtr4d
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` n ) <_ ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` ( n + 1 ) ) )
50 1 6 49 monoordxrv
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` M ) <_ ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` N ) )
51 eluzfz1
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
52 1 51 syl
 |-  ( ph -> M e. ( M ... N ) )
53 fveq2
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
54 53 xnegeqd
 |-  ( k = M -> -e ( F ` k ) = -e ( F ` M ) )
55 xnegex
 |-  -e ( F ` M ) e. _V
56 54 41 55 fvmpt
 |-  ( M e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` M ) = -e ( F ` M ) )
57 52 56 syl
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` M ) = -e ( F ` M ) )
58 eluzfz2
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
59 1 58 syl
 |-  ( ph -> N e. ( M ... N ) )
60 fveq2
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
61 60 xnegeqd
 |-  ( k = N -> -e ( F ` k ) = -e ( F ` N ) )
62 xnegex
 |-  -e ( F ` N ) e. _V
63 61 41 62 fvmpt
 |-  ( N e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` N ) = -e ( F ` N ) )
64 59 63 syl
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -e ( F ` k ) ) ` N ) = -e ( F ` N ) )
65 50 57 64 3brtr3d
 |-  ( ph -> -e ( F ` M ) <_ -e ( F ` N ) )
66 60 eleq1d
 |-  ( k = N -> ( ( F ` k ) e. RR* <-> ( F ` N ) e. RR* ) )
67 66 rspcv
 |-  ( N e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` N ) e. RR* ) )
68 59 25 67 sylc
 |-  ( ph -> ( F ` N ) e. RR* )
69 53 eleq1d
 |-  ( k = M -> ( ( F ` k ) e. RR* <-> ( F ` M ) e. RR* ) )
70 69 rspcv
 |-  ( M e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` M ) e. RR* ) )
71 52 25 70 sylc
 |-  ( ph -> ( F ` M ) e. RR* )
72 xleneg
 |-  ( ( ( F ` N ) e. RR* /\ ( F ` M ) e. RR* ) -> ( ( F ` N ) <_ ( F ` M ) <-> -e ( F ` M ) <_ -e ( F ` N ) ) )
73 68 71 72 syl2anc
 |-  ( ph -> ( ( F ` N ) <_ ( F ` M ) <-> -e ( F ` M ) <_ -e ( F ` N ) ) )
74 65 73 mpbird
 |-  ( ph -> ( F ` N ) <_ ( F ` M ) )