Metamath Proof Explorer

Theorem monoord

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 9-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 monoord.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 monoord.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
3 monoord.3 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
4 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
5 1 4 syl 
 |-  ( ph -> N e. ( M ... N ) )
6 eleq1 
 |-  ( x = M -> ( x e. ( M ... N ) <-> M e. ( M ... N ) ) )
7 fveq2 
 |-  ( x = M -> ( F ` x ) = ( F ` M ) )
8 7 breq2d 
 |-  ( x = M -> ( ( F ` M ) <_ ( F ` x ) <-> ( F ` M ) <_ ( F ` M ) ) )
9 6 8 imbi12d 
 |-  ( x = M -> ( ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) <-> ( M e. ( M ... N ) -> ( F ` M ) <_ ( F ` M ) ) ) )
10 9 imbi2d 
 |-  ( x = M -> ( ( ph -> ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) ) <-> ( ph -> ( M e. ( M ... N ) -> ( F ` M ) <_ ( F ` M ) ) ) ) )
11 eleq1 
 |-  ( x = n -> ( x e. ( M ... N ) <-> n e. ( M ... N ) ) )
12 fveq2 
 |-  ( x = n -> ( F ` x ) = ( F ` n ) )
13 12 breq2d 
 |-  ( x = n -> ( ( F ` M ) <_ ( F ` x ) <-> ( F ` M ) <_ ( F ` n ) ) )
14 11 13 imbi12d 
 |-  ( x = n -> ( ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) <-> ( n e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) ) )
15 14 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) ) <-> ( ph -> ( n e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) ) ) )
16 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( M ... N ) <-> ( n + 1 ) e. ( M ... N ) ) )
17 fveq2 
 |-  ( x = ( n + 1 ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
18 17 breq2d 
 |-  ( x = ( n + 1 ) -> ( ( F ` M ) <_ ( F ` x ) <-> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) )
19 16 18 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) <-> ( ( n + 1 ) e. ( M ... N ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) ) )
20 19 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) ) ) )
21 eleq1 
 |-  ( x = N -> ( x e. ( M ... N ) <-> N e. ( M ... N ) ) )
22 fveq2 
 |-  ( x = N -> ( F ` x ) = ( F ` N ) )
23 22 breq2d 
 |-  ( x = N -> ( ( F ` M ) <_ ( F ` x ) <-> ( F ` M ) <_ ( F ` N ) ) )
24 21 23 imbi12d 
 |-  ( x = N -> ( ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) <-> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) ) )
25 24 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( M ... N ) -> ( F ` M ) <_ ( F ` x ) ) ) <-> ( ph -> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) ) ) )
26 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
27 26 eleq1d 
 |-  ( k = M -> ( ( F ` k ) e. RR <-> ( F ` M ) e. RR ) )
28 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) e. RR )
29 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
30 1 29 syl 
 |-  ( ph -> M e. ( M ... N ) )
31 27 28 30 rspcdva 
 |-  ( ph -> ( F ` M ) e. RR )
32 31 leidd 
 |-  ( ph -> ( F ` M ) <_ ( F ` M ) )
33 32 a1d 
 |-  ( ph -> ( M e. ( M ... N ) -> ( F ` M ) <_ ( F ` M ) ) )
34 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
35 34 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... N ) )
36 35 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n + 1 ) e. ( M ... N ) -> n e. ( M ... N ) ) )
37 36 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) -> ( ( n + 1 ) e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) ) )
38 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
39 fvoveq1 
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
40 38 39 breq12d 
 |-  ( k = n -> ( ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> ( F ` n ) <_ ( F ` ( n + 1 ) ) ) )
41 3 ralrimiva 
 |-  ( ph -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) <_ ( F ` ( k + 1 ) ) )
42 41 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) <_ ( F ` ( k + 1 ) ) )
43 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( ZZ>= ` M ) )
44 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
45 43 44 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ZZ )
46 simprr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( M ... N ) )
47 elfzuz3 
 |-  ( ( n + 1 ) e. ( M ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
48 46 47 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
49 eluzp1m1 
 |-  ( ( n e. ZZ /\ N e. ( ZZ>= ` ( n + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
50 45 48 49 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
51 elfzuzb 
 |-  ( n e. ( M ... ( N - 1 ) ) <-> ( n e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` n ) ) )
52 43 50 51 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... ( N - 1 ) ) )
53 40 42 52 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
54 31 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` M ) e. RR )
55 38 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. RR <-> ( F ` n ) e. RR ) )
56 28 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. k e. ( M ... N ) ( F ` k ) e. RR )
57 55 56 35 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` n ) e. RR )
58 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
59 58 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( n + 1 ) ) e. RR ) )
60 59 56 46 rspcdva 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) e. RR )
61 letr 
 |-  ( ( ( F ` M ) e. RR /\ ( F ` n ) e. RR /\ ( F ` ( n + 1 ) ) e. RR ) -> ( ( ( F ` M ) <_ ( F ` n ) /\ ( F ` n ) <_ ( F ` ( n + 1 ) ) ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) )
62 54 57 60 61 syl3anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( ( F ` M ) <_ ( F ` n ) /\ ( F ` n ) <_ ( F ` ( n + 1 ) ) ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) )
63 53 62 mpan2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( F ` M ) <_ ( F ` n ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) )
64 37 63 animpimp2impd 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( n e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) ) -> ( ph -> ( ( n + 1 ) e. ( M ... N ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) ) ) )
65 10 15 20 25 33 64 uzind4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) ) )
66 1 65 mpcom 
 |-  ( ph -> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) )
67 5 66 mpd 
 |-  ( ph -> ( F ` M ) <_ ( F ` N ) )