Metamath Proof Explorer

Theorem smonoord

Description: Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord (except that the case M = N must be excluded). Duplicate of monoords ? (Contributed by AV, 12-Jul-2020)

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

Proof

Step Hyp Ref Expression
1 smonoord.0 
 |-  ( ph -> M e. ZZ )
2 smonoord.1 
 |-  ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )
3 smonoord.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
4 smonoord.3 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )
5 eluzfz2 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ( ( M + 1 ) ... N ) )
6 2 5 syl 
 |-  ( ph -> N e. ( ( M + 1 ) ... N ) )
7 eleq1 
 |-  ( x = ( M + 1 ) -> ( x e. ( ( M + 1 ) ... N ) <-> ( M + 1 ) e. ( ( M + 1 ) ... N ) ) )
8 fveq2 
 |-  ( x = ( M + 1 ) -> ( F ` x ) = ( F ` ( M + 1 ) ) )
9 8 breq2d 
 |-  ( x = ( M + 1 ) -> ( ( F ` M ) < ( F ` x ) <-> ( F ` M ) < ( F ` ( M + 1 ) ) ) )
10 7 9 imbi12d 
 |-  ( x = ( M + 1 ) -> ( ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) <-> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( M + 1 ) ) ) ) )
11 10 imbi2d 
 |-  ( x = ( M + 1 ) -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) ) <-> ( ph -> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( M + 1 ) ) ) ) ) )
12 eleq1 
 |-  ( x = n -> ( x e. ( ( M + 1 ) ... N ) <-> n e. ( ( M + 1 ) ... N ) ) )
13 fveq2 
 |-  ( x = n -> ( F ` x ) = ( F ` n ) )
14 13 breq2d 
 |-  ( x = n -> ( ( F ` M ) < ( F ` x ) <-> ( F ` M ) < ( F ` n ) ) )
15 12 14 imbi12d 
 |-  ( x = n -> ( ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) <-> ( n e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` n ) ) ) )
16 15 imbi2d 
 |-  ( x = n -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) ) <-> ( ph -> ( n e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` n ) ) ) ) )
17 eleq1 
 |-  ( x = ( n + 1 ) -> ( x e. ( ( M + 1 ) ... N ) <-> ( n + 1 ) e. ( ( M + 1 ) ... N ) ) )
18 fveq2 
 |-  ( x = ( n + 1 ) -> ( F ` x ) = ( F ` ( n + 1 ) ) )
19 18 breq2d 
 |-  ( x = ( n + 1 ) -> ( ( F ` M ) < ( F ` x ) <-> ( F ` M ) < ( F ` ( n + 1 ) ) ) )
20 17 19 imbi12d 
 |-  ( x = ( n + 1 ) -> ( ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) <-> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( n + 1 ) ) ) ) )
21 20 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( n + 1 ) ) ) ) ) )
22 eleq1 
 |-  ( x = N -> ( x e. ( ( M + 1 ) ... N ) <-> N e. ( ( M + 1 ) ... N ) ) )
23 fveq2 
 |-  ( x = N -> ( F ` x ) = ( F ` N ) )
24 23 breq2d 
 |-  ( x = N -> ( ( F ` M ) < ( F ` x ) <-> ( F ` M ) < ( F ` N ) ) )
25 22 24 imbi12d 
 |-  ( x = N -> ( ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) <-> ( N e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` N ) ) ) )
26 25 imbi2d 
 |-  ( x = N -> ( ( ph -> ( x e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` x ) ) ) <-> ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` N ) ) ) ) )
27 eluzp1m1 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
28 1 2 27 syl2anc 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` M ) )
29 eluzfz1 
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> M e. ( M ... ( N - 1 ) ) )
30 28 29 syl 
 |-  ( ph -> M e. ( M ... ( N - 1 ) ) )
31 4 ralrimiva 
 |-  ( ph -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) < ( F ` ( k + 1 ) ) )
32 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
33 fvoveq1 
 |-  ( k = M -> ( F ` ( k + 1 ) ) = ( F ` ( M + 1 ) ) )
34 32 33 breq12d 
 |-  ( k = M -> ( ( F ` k ) < ( F ` ( k + 1 ) ) <-> ( F ` M ) < ( F ` ( M + 1 ) ) ) )
35 34 rspcv 
 |-  ( M e. ( M ... ( N - 1 ) ) -> ( A. k e. ( M ... ( N - 1 ) ) ( F ` k ) < ( F ` ( k + 1 ) ) -> ( F ` M ) < ( F ` ( M + 1 ) ) ) )
36 30 31 35 sylc 
 |-  ( ph -> ( F ` M ) < ( F ` ( M + 1 ) ) )
37 36 a1d 
 |-  ( ph -> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( M + 1 ) ) ) )
38 37 a1i 
 |-  ( ( M + 1 ) e. ZZ -> ( ph -> ( ( M + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( M + 1 ) ) ) ) )
39 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> n e. ( ( M + 1 ) ... N ) )
40 39 adantll 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` ( M + 1 ) ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> n e. ( ( M + 1 ) ... N ) )
41 40 ex 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> n e. ( ( M + 1 ) ... N ) ) )
42 41 imim1d 
 |-  ( ( ph /\ n e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( n e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` n ) ) -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` n ) ) ) )
43 peano2uzr 
 |-  ( ( M e. ZZ /\ n e. ( ZZ>= ` ( M + 1 ) ) ) -> n e. ( ZZ>= ` M ) )
44 43 ex 
 |-  ( M e. ZZ -> ( n e. ( ZZ>= ` ( M + 1 ) ) -> n e. ( ZZ>= ` M ) ) )
45 44 1 syl11 
 |-  ( n e. ( ZZ>= ` ( M + 1 ) ) -> ( ph -> n e. ( ZZ>= ` M ) ) )
46 45 adantr 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> ( ph -> n e. ( ZZ>= ` M ) ) )
47 46 impcom 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( ZZ>= ` M ) )
48 eluzelz 
 |-  ( n e. ( ZZ>= ` ( M + 1 ) ) -> n e. ZZ )
49 48 adantr 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> n e. ZZ )
50 49 adantl 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ZZ )
51 elfzuz3 
 |-  ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
52 51 ad2antll 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> N e. ( ZZ>= ` ( n + 1 ) ) )
53 eluzp1m1 
 |-  ( ( n e. ZZ /\ N e. ( ZZ>= ` ( n + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
54 50 52 53 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( N - 1 ) e. ( ZZ>= ` n ) )
55 elfzuzb 
 |-  ( n e. ( M ... ( N - 1 ) ) <-> ( n e. ( ZZ>= ` M ) /\ ( N - 1 ) e. ( ZZ>= ` n ) ) )
56 47 54 55 sylanbrc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( M ... ( N - 1 ) ) )
57 31 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> A. k e. ( M ... ( N - 1 ) ) ( F ` k ) < ( F ` ( k + 1 ) ) )
58 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
59 fvoveq1 
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
60 58 59 breq12d 
 |-  ( k = n -> ( ( F ` k ) < ( F ` ( k + 1 ) ) <-> ( F ` n ) < ( F ` ( n + 1 ) ) ) )
61 60 rspcv 
 |-  ( n e. ( M ... ( N - 1 ) ) -> ( A. k e. ( M ... ( N - 1 ) ) ( F ` k ) < ( F ` ( k + 1 ) ) -> ( F ` n ) < ( F ` ( n + 1 ) ) ) )
62 56 57 61 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( F ` n ) < ( F ` ( n + 1 ) ) )
63 zre 
 |-  ( M e. ZZ -> M e. RR )
64 63 lep1d 
 |-  ( M e. ZZ -> M <_ ( M + 1 ) )
65 1 64 jccir 
 |-  ( ph -> ( M e. ZZ /\ M <_ ( M + 1 ) ) )
66 eluzuzle 
 |-  ( ( M e. ZZ /\ M <_ ( M + 1 ) ) -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> N e. ( ZZ>= ` M ) ) )
67 65 2 66 sylc 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
68 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
69 67 68 syl 
 |-  ( ph -> M e. ( M ... N ) )
70 3 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) ( F ` k ) e. RR )
71 32 eleq1d 
 |-  ( k = M -> ( ( F ` k ) e. RR <-> ( F ` M ) e. RR ) )
72 71 rspcv 
 |-  ( M e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR -> ( F ` M ) e. RR ) )
73 69 70 72 sylc 
 |-  ( ph -> ( F ` M ) e. RR )
74 73 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( F ` M ) e. RR )
75 fzp1ss 
 |-  ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
76 1 75 syl 
 |-  ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
77 76 sseld 
 |-  ( ph -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( n + 1 ) e. ( M ... N ) ) )
78 77 com12 
 |-  ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( ph -> ( n + 1 ) e. ( M ... N ) ) )
79 78 adantl 
 |-  ( ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) -> ( ph -> ( n + 1 ) e. ( M ... N ) ) )
80 79 impcom 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( n + 1 ) e. ( M ... N ) )
81 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ( n + 1 ) e. ( M ... N ) ) -> n e. ( M ... N ) )
82 47 80 81 syl2anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> n e. ( M ... N ) )
83 70 adantr 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> A. k e. ( M ... N ) ( F ` k ) e. RR )
84 58 eleq1d 
 |-  ( k = n -> ( ( F ` k ) e. RR <-> ( F ` n ) e. RR ) )
85 84 rspcv 
 |-  ( n e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR -> ( F ` n ) e. RR ) )
86 82 83 85 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( F ` n ) e. RR )
87 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
88 87 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( n + 1 ) ) e. RR ) )
89 88 rspcv 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( A. k e. ( M ... N ) ( F ` k ) e. RR -> ( F ` ( n + 1 ) ) e. RR ) )
90 80 83 89 sylc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( F ` ( n + 1 ) ) e. RR )
91 lttr 
 |-  ( ( ( 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 ) ) ) )
92 74 86 90 91 syl3anc 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( ( F ` M ) < ( F ` n ) /\ ( F ` n ) < ( F ` ( n + 1 ) ) ) -> ( F ` M ) < ( F ` ( n + 1 ) ) ) )
93 62 92 mpan2d 
 |-  ( ( ph /\ ( n e. ( ZZ>= ` ( M + 1 ) ) /\ ( n + 1 ) e. ( ( M + 1 ) ... N ) ) ) -> ( ( F ` M ) < ( F ` n ) -> ( F ` M ) < ( F ` ( n + 1 ) ) ) )
94 42 93 animpimp2impd 
 |-  ( n e. ( ZZ>= ` ( M + 1 ) ) -> ( ( ph -> ( n e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` n ) ) ) -> ( ph -> ( ( n + 1 ) e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` ( n + 1 ) ) ) ) ) )
95 11 16 21 26 38 94 uzind4 
 |-  ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` N ) ) ) )
96 2 95 mpcom 
 |-  ( ph -> ( N e. ( ( M + 1 ) ... N ) -> ( F ` M ) < ( F ` N ) ) )
97 6 96 mpd 
 |-  ( ph -> ( F ` M ) < ( F ` N ) )