Metamath Proof Explorer

Theorem monoord2

Description: Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014)

Ref Expression
Hypotheses monoord2.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
monoord2.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
monoord2.3 
|- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
Assertion monoord2 
|- ( ph -> ( F ` N ) <_ ( F ` M ) )

Proof

Step Hyp Ref Expression
1 monoord2.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 monoord2.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
3 monoord2.3 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
4 2 renegcld 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> -u ( F ` k ) e. RR )
5 4 fmpttd 
 |-  ( ph -> ( k e. ( M ... N ) |-> -u ( F ` k ) ) : ( M ... N ) --> RR )
6 5 ffvelcdmda 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( ( k e. ( M ... N ) |-> -u ( 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 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
15 14 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( n + 1 ) ) e. RR ) )
16 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) e. RR )
17 16 adantr 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> A. k e. ( M ... N ) ( F ` k ) e. RR )
18 fzp1elp1 
 |-  ( n e. ( M ... ( N - 1 ) ) -> ( n + 1 ) e. ( M ... ( ( N - 1 ) + 1 ) ) )
19 18 adantl 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( M ... ( ( N - 1 ) + 1 ) ) )
20 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
21 1 20 syl 
 |-  ( ph -> N e. ZZ )
22 21 zcnd 
 |-  ( ph -> N e. CC )
23 ax-1cn 
 |-  1 e. CC
24 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
25 22 23 24 sylancl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
26 25 oveq2d 
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
27 26 adantr 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
28 19 27 eleqtrd 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( M ... N ) )
29 15 17 28 rspcdva 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` ( n + 1 ) ) e. RR )
30 9 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. RR <-> ( F ` n ) e. RR ) )
31 fzssp1 
 |-  ( M ... ( N - 1 ) ) C_ ( M ... ( ( N - 1 ) + 1 ) )
32 31 26 sseqtrid 
 |-  ( ph -> ( M ... ( N - 1 ) ) C_ ( M ... N ) )
33 32 sselda 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ( M ... N ) )
34 30 17 33 rspcdva 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` n ) e. RR )
35 29 34 lenegd 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( F ` ( n + 1 ) ) <_ ( F ` n ) <-> -u ( F ` n ) <_ -u ( F ` ( n + 1 ) ) ) )
36 13 35 mpbid 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> -u ( F ` n ) <_ -u ( F ` ( n + 1 ) ) )
37 9 negeqd 
 |-  ( k = n -> -u ( F ` k ) = -u ( F ` n ) )
38 eqid 
 |-  ( k e. ( M ... N ) |-> -u ( F ` k ) ) = ( k e. ( M ... N ) |-> -u ( F ` k ) )
39 negex 
 |-  -u ( F ` n ) e. _V
40 37 38 39 fvmpt 
 |-  ( n e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` n ) = -u ( F ` n ) )
41 33 40 syl 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` n ) = -u ( F ` n ) )
42 14 negeqd 
 |-  ( k = ( n + 1 ) -> -u ( F ` k ) = -u ( F ` ( n + 1 ) ) )
43 negex 
 |-  -u ( F ` ( n + 1 ) ) e. _V
44 42 38 43 fvmpt 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` ( n + 1 ) ) = -u ( F ` ( n + 1 ) ) )
45 28 44 syl 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` ( n + 1 ) ) = -u ( F ` ( n + 1 ) ) )
46 36 41 45 3brtr4d 
 |-  ( ( ph /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` n ) <_ ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` ( n + 1 ) ) )
47 1 6 46 monoord 
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` M ) <_ ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` N ) )
48 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
49 1 48 syl 
 |-  ( ph -> M e. ( M ... N ) )
50 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
51 50 negeqd 
 |-  ( k = M -> -u ( F ` k ) = -u ( F ` M ) )
52 negex 
 |-  -u ( F ` M ) e. _V
53 51 38 52 fvmpt 
 |-  ( M e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` M ) = -u ( F ` M ) )
54 49 53 syl 
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` M ) = -u ( F ` M ) )
55 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
56 1 55 syl 
 |-  ( ph -> N e. ( M ... N ) )
57 fveq2 
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
58 57 negeqd 
 |-  ( k = N -> -u ( F ` k ) = -u ( F ` N ) )
59 negex 
 |-  -u ( F ` N ) e. _V
60 58 38 59 fvmpt 
 |-  ( N e. ( M ... N ) -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` N ) = -u ( F ` N ) )
61 56 60 syl 
 |-  ( ph -> ( ( k e. ( M ... N ) |-> -u ( F ` k ) ) ` N ) = -u ( F ` N ) )
62 47 54 61 3brtr3d 
 |-  ( ph -> -u ( F ` M ) <_ -u ( F ` N ) )
63 57 eleq1d 
 |-  ( k = N -> ( ( F ` k ) e. RR <-> ( F ` N ) e. RR ) )
64 63 16 56 rspcdva 
 |-  ( ph -> ( F ` N ) e. RR )
65 50 eleq1d 
 |-  ( k = M -> ( ( F ` k ) e. RR <-> ( F ` M ) e. RR ) )
66 65 16 49 rspcdva 
 |-  ( ph -> ( F ` M ) e. RR )
67 64 66 lenegd 
 |-  ( ph -> ( ( F ` N ) <_ ( F ` M ) <-> -u ( F ` M ) <_ -u ( F ` N ) ) )
68 62 67 mpbird 
 |-  ( ph -> ( F ` N ) <_ ( F ` M ) )