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