Metamath Proof Explorer

Theorem monoordxrv

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

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

Proof

Step Hyp Ref Expression
1 monoordxrv.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 monoordxrv.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR* )
3 monoordxrv.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 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
27 1 26 syl 
 |-  ( ph -> M e. ( M ... N ) )
28 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) e. RR* )
29 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
30 29 eleq1d 
 |-  ( k = M -> ( ( F ` k ) e. RR* <-> ( F ` M ) e. RR* ) )
31 30 rspcv 
 |-  ( M e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` M ) e. RR* ) )
32 27 28 31 sylc 
 |-  ( ph -> ( F ` M ) e. RR* )
33 32 xrleidd 
 |-  ( ph -> ( F ` M ) <_ ( F ` M ) )
34 33 a1d 
 |-  ( ph -> ( M e. ( M ... N ) -> ( F ` M ) <_ ( F ` M ) ) )
35 34 a1i 
 |-  ( M e. ZZ -> ( ph -> ( M e. ( M ... N ) -> ( F ` M ) <_ ( F ` M ) ) ) )
36 simprl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( ZZ>= ` M ) )
37 simprr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( n + 1 ) e. ( M ... N ) )
38 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
39 36 37 38 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... N ) )
40 39 expr 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n + 1 ) e. ( M ... N ) -> n e. ( M ... N ) ) )
41 40 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( ( n e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) -> ( ( n + 1 ) e. ( M ... N ) -> ( F ` M ) <_ ( F ` n ) ) ) )
42 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
43 36 42 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ZZ )
44 elfzuz3 
 |-  ( ( n + 1 ) e. ( M ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
45 37 44 syl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
46 eluzp1m1 
 |-  ( ( n e. ZZ /\ N e. ( ZZ>= ` ( n + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
47 43 45 46 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
48 elfzuzb 
 |-  ( n e. ( M ... ( N - 1 ) ) <-> ( n e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` n ) ) )
49 36 47 48 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> n e. ( M ... ( N - 1 ) ) )
50 3 ralrimiva 
 |-  ( ph -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) <_ ( F ` ( k + 1 ) ) )
51 50 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) <_ ( F ` ( k + 1 ) ) )
52 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
53 fvoveq1 
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
54 52 53 breq12d 
 |-  ( k = n -> ( ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> ( F ` n ) <_ ( F ` ( n + 1 ) ) ) )
55 54 rspcv 
 |-  ( n e. ( M ... ( N - 1 ) ) -> ( A. k e. ( M ... ( N - 1 ) ) ( F ` k ) <_ ( F ` ( k + 1 ) ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) ) )
56 49 51 55 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
57 32 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` M ) e. RR* )
58 28 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> A. k e. ( M ... N ) ( F ` k ) e. RR* )
59 52 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. RR* <-> ( F ` n ) e. RR* ) )
60 59 rspcv 
 |-  ( n e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` n ) e. RR* ) )
61 39 58 60 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` n ) e. RR* )
62 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
63 62 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. RR* <-> ( F ` ( n + 1 ) ) e. RR* ) )
64 63 rspcv 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR* -> ( F ` ( n + 1 ) ) e. RR* ) )
65 37 58 64 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( F ` ( n + 1 ) ) e. RR* )
66 xrletr 
 |-  ( ( ( 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 ) ) ) )
67 57 61 65 66 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 ) ) ) )
68 56 67 mpan2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) ) -> ( ( F ` M ) <_ ( F ` n ) -> ( F ` M ) <_ ( F ` ( n + 1 ) ) ) )
69 41 68 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 ) ) ) ) ) )
70 10 15 20 25 35 69 uzind4 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) ) )
71 1 70 mpcom 
 |-  ( ph -> ( N e. ( M ... N ) -> ( F ` M ) <_ ( F ` N ) ) )
72 5 71 mpd 
 |-  ( ph -> ( F ` M ) <_ ( F ` N ) )