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

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