Metamath Proof Explorer

Theorem monoords

Description: Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses monoords.fk 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
monoords.flt 
|- ( ( ph /\ k e. ( M ..^ N ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )
monoords.i 
|- ( ph -> I e. ( M ... N ) )
monoords.j 
|- ( ph -> J e. ( M ... N ) )
monoords.iltj 
|- ( ph -> I < J )
Assertion monoords 
|- ( ph -> ( F ` I ) < ( F ` J ) )

Proof

Step Hyp Ref Expression
1 monoords.fk 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )
2 monoords.flt 
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )
3 monoords.i 
 |-  ( ph -> I e. ( M ... N ) )
4 monoords.j 
 |-  ( ph -> J e. ( M ... N ) )
5 monoords.iltj 
 |-  ( ph -> I < J )
6 3 ancli 
 |-  ( ph -> ( ph /\ I e. ( M ... N ) ) )
7 eleq1 
 |-  ( k = I -> ( k e. ( M ... N ) <-> I e. ( M ... N ) ) )
8 7 anbi2d 
 |-  ( k = I -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ I e. ( M ... N ) ) ) )
9 fveq2 
 |-  ( k = I -> ( F ` k ) = ( F ` I ) )
10 9 eleq1d 
 |-  ( k = I -> ( ( F ` k ) e. RR <-> ( F ` I ) e. RR ) )
11 8 10 imbi12d 
 |-  ( k = I -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ I e. ( M ... N ) ) -> ( F ` I ) e. RR ) ) )
12 11 1 vtoclg 
 |-  ( I e. ( M ... N ) -> ( ( ph /\ I e. ( M ... N ) ) -> ( F ` I ) e. RR ) )
13 3 6 12 sylc 
 |-  ( ph -> ( F ` I ) e. RR )
14 elfzel1 
 |-  ( I e. ( M ... N ) -> M e. ZZ )
15 3 14 syl 
 |-  ( ph -> M e. ZZ )
16 elfzelz 
 |-  ( I e. ( M ... N ) -> I e. ZZ )
17 3 16 syl 
 |-  ( ph -> I e. ZZ )
18 elfzle1 
 |-  ( I e. ( M ... N ) -> M <_ I )
19 3 18 syl 
 |-  ( ph -> M <_ I )
20 eluz2 
 |-  ( I e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ I e. ZZ /\ M <_ I ) )
21 15 17 19 20 syl3anbrc 
 |-  ( ph -> I e. ( ZZ>= ` M ) )
22 elfzuz2 
 |-  ( I e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
23 3 22 syl 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
24 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
25 23 24 syl 
 |-  ( ph -> N e. ZZ )
26 17 zred 
 |-  ( ph -> I e. RR )
27 elfzelz 
 |-  ( J e. ( M ... N ) -> J e. ZZ )
28 4 27 syl 
 |-  ( ph -> J e. ZZ )
29 28 zred 
 |-  ( ph -> J e. RR )
30 25 zred 
 |-  ( ph -> N e. RR )
31 elfzle2 
 |-  ( J e. ( M ... N ) -> J <_ N )
32 4 31 syl 
 |-  ( ph -> J <_ N )
33 26 29 30 5 32 ltletrd 
 |-  ( ph -> I < N )
34 elfzo2 
 |-  ( I e. ( M ..^ N ) <-> ( I e. ( ZZ>= ` M ) /\ N e. ZZ /\ I < N ) )
35 21 25 33 34 syl3anbrc 
 |-  ( ph -> I e. ( M ..^ N ) )
36 fzofzp1 
 |-  ( I e. ( M ..^ N ) -> ( I + 1 ) e. ( M ... N ) )
37 35 36 syl 
 |-  ( ph -> ( I + 1 ) e. ( M ... N ) )
38 37 ancli 
 |-  ( ph -> ( ph /\ ( I + 1 ) e. ( M ... N ) ) )
39 eleq1 
 |-  ( k = ( I + 1 ) -> ( k e. ( M ... N ) <-> ( I + 1 ) e. ( M ... N ) ) )
40 39 anbi2d 
 |-  ( k = ( I + 1 ) -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ ( I + 1 ) e. ( M ... N ) ) ) )
41 fveq2 
 |-  ( k = ( I + 1 ) -> ( F ` k ) = ( F ` ( I + 1 ) ) )
42 41 eleq1d 
 |-  ( k = ( I + 1 ) -> ( ( F ` k ) e. RR <-> ( F ` ( I + 1 ) ) e. RR ) )
43 40 42 imbi12d 
 |-  ( k = ( I + 1 ) -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ ( I + 1 ) e. ( M ... N ) ) -> ( F ` ( I + 1 ) ) e. RR ) ) )
44 43 1 vtoclg 
 |-  ( ( I + 1 ) e. ( M ... N ) -> ( ( ph /\ ( I + 1 ) e. ( M ... N ) ) -> ( F ` ( I + 1 ) ) e. RR ) )
45 37 38 44 sylc 
 |-  ( ph -> ( F ` ( I + 1 ) ) e. RR )
46 4 ancli 
 |-  ( ph -> ( ph /\ J e. ( M ... N ) ) )
47 eleq1 
 |-  ( k = J -> ( k e. ( M ... N ) <-> J e. ( M ... N ) ) )
48 47 anbi2d 
 |-  ( k = J -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ J e. ( M ... N ) ) ) )
49 fveq2 
 |-  ( k = J -> ( F ` k ) = ( F ` J ) )
50 49 eleq1d 
 |-  ( k = J -> ( ( F ` k ) e. RR <-> ( F ` J ) e. RR ) )
51 48 50 imbi12d 
 |-  ( k = J -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ J e. ( M ... N ) ) -> ( F ` J ) e. RR ) ) )
52 51 1 vtoclg 
 |-  ( J e. ( M ... N ) -> ( ( ph /\ J e. ( M ... N ) ) -> ( F ` J ) e. RR ) )
53 4 46 52 sylc 
 |-  ( ph -> ( F ` J ) e. RR )
54 35 ancli 
 |-  ( ph -> ( ph /\ I e. ( M ..^ N ) ) )
55 eleq1 
 |-  ( k = I -> ( k e. ( M ..^ N ) <-> I e. ( M ..^ N ) ) )
56 55 anbi2d 
 |-  ( k = I -> ( ( ph /\ k e. ( M ..^ N ) ) <-> ( ph /\ I e. ( M ..^ N ) ) ) )
57 fvoveq1 
 |-  ( k = I -> ( F ` ( k + 1 ) ) = ( F ` ( I + 1 ) ) )
58 9 57 breq12d 
 |-  ( k = I -> ( ( F ` k ) < ( F ` ( k + 1 ) ) <-> ( F ` I ) < ( F ` ( I + 1 ) ) ) )
59 56 58 imbi12d 
 |-  ( k = I -> ( ( ( ph /\ k e. ( M ..^ N ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) ) <-> ( ( ph /\ I e. ( M ..^ N ) ) -> ( F ` I ) < ( F ` ( I + 1 ) ) ) ) )
60 59 2 vtoclg 
 |-  ( I e. ( M ..^ N ) -> ( ( ph /\ I e. ( M ..^ N ) ) -> ( F ` I ) < ( F ` ( I + 1 ) ) ) )
61 35 54 60 sylc 
 |-  ( ph -> ( F ` I ) < ( F ` ( I + 1 ) ) )
62 17 peano2zd 
 |-  ( ph -> ( I + 1 ) e. ZZ )
63 zltp1le 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I < J <-> ( I + 1 ) <_ J ) )
64 17 28 63 syl2anc 
 |-  ( ph -> ( I < J <-> ( I + 1 ) <_ J ) )
65 5 64 mpbid 
 |-  ( ph -> ( I + 1 ) <_ J )
66 eluz2 
 |-  ( J e. ( ZZ>= ` ( I + 1 ) ) <-> ( ( I + 1 ) e. ZZ /\ J e. ZZ /\ ( I + 1 ) <_ J ) )
67 62 28 65 66 syl3anbrc 
 |-  ( ph -> J e. ( ZZ>= ` ( I + 1 ) ) )
68 15 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M e. ZZ )
69 25 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> N e. ZZ )
70 elfzelz 
 |-  ( k e. ( ( I + 1 ) ... J ) -> k e. ZZ )
71 70 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> k e. ZZ )
72 68 69 71 3jca 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
73 68 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M e. RR )
74 71 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> k e. RR )
75 62 zred 
 |-  ( ph -> ( I + 1 ) e. RR )
76 75 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> ( I + 1 ) e. RR )
77 26 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> I e. RR )
78 19 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M <_ I )
79 77 ltp1d 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> I < ( I + 1 ) )
80 73 77 76 78 79 lelttrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M < ( I + 1 ) )
81 elfzle1 
 |-  ( k e. ( ( I + 1 ) ... J ) -> ( I + 1 ) <_ k )
82 81 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> ( I + 1 ) <_ k )
83 73 76 74 80 82 ltletrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M < k )
84 73 74 83 ltled 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> M <_ k )
85 29 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> J e. RR )
86 69 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> N e. RR )
87 elfzle2 
 |-  ( k e. ( ( I + 1 ) ... J ) -> k <_ J )
88 87 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> k <_ J )
89 32 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> J <_ N )
90 74 85 86 88 89 letrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> k <_ N )
91 72 84 90 jca32 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> ( ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ N ) ) )
92 elfz2 
 |-  ( k e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ N ) ) )
93 91 92 sylibr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> k e. ( M ... N ) )
94 93 1 syldan 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... J ) ) -> ( F ` k ) e. RR )
95 15 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> M e. ZZ )
96 25 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> N e. ZZ )
97 elfzelz 
 |-  ( k e. ( ( I + 1 ) ... ( J - 1 ) ) -> k e. ZZ )
98 97 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k e. ZZ )
99 95 96 98 3jca 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) )
100 95 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> M e. RR )
101 98 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k e. RR )
102 75 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( I + 1 ) e. RR )
103 15 zred 
 |-  ( ph -> M e. RR )
104 26 ltp1d 
 |-  ( ph -> I < ( I + 1 ) )
105 103 26 75 19 104 lelttrd 
 |-  ( ph -> M < ( I + 1 ) )
106 105 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> M < ( I + 1 ) )
107 elfzle1 
 |-  ( k e. ( ( I + 1 ) ... ( J - 1 ) ) -> ( I + 1 ) <_ k )
108 107 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( I + 1 ) <_ k )
109 100 102 101 106 108 ltletrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> M < k )
110 100 101 109 ltled 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> M <_ k )
111 96 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> N e. RR )
112 peano2rem 
 |-  ( J e. RR -> ( J - 1 ) e. RR )
113 29 112 syl 
 |-  ( ph -> ( J - 1 ) e. RR )
114 113 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( J - 1 ) e. RR )
115 elfzle2 
 |-  ( k e. ( ( I + 1 ) ... ( J - 1 ) ) -> k <_ ( J - 1 ) )
116 115 adantl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k <_ ( J - 1 ) )
117 29 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> J e. RR )
118 117 ltm1d 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( J - 1 ) < J )
119 32 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> J <_ N )
120 114 117 111 118 119 ltletrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( J - 1 ) < N )
121 101 114 111 116 120 lelttrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k < N )
122 101 111 121 ltled 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k <_ N )
123 99 110 122 jca32 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( ( M e. ZZ /\ N e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ N ) ) )
124 123 92 sylibr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k e. ( M ... N ) )
125 124 1 syldan 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( F ` k ) e. RR )
126 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
127 96 126 syl 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( N - 1 ) e. ZZ )
128 95 127 98 3jca 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ k e. ZZ ) )
129 127 zred 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( N - 1 ) e. RR )
130 1red 
 |-  ( ph -> 1 e. RR )
131 29 30 130 32 lesub1dd 
 |-  ( ph -> ( J - 1 ) <_ ( N - 1 ) )
132 131 adantr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( J - 1 ) <_ ( N - 1 ) )
133 101 114 129 116 132 letrd 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k <_ ( N - 1 ) )
134 128 110 133 jca32 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ ( N - 1 ) ) ) )
135 elfz2 
 |-  ( k e. ( M ... ( N - 1 ) ) <-> ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ k e. ZZ ) /\ ( M <_ k /\ k <_ ( N - 1 ) ) ) )
136 134 135 sylibr 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> k e. ( M ... ( N - 1 ) ) )
137 simpr 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> k e. ( M ... ( N - 1 ) ) )
138 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
139 25 138 syl 
 |-  ( ph -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
140 139 eqcomd 
 |-  ( ph -> ( M ... ( N - 1 ) ) = ( M ..^ N ) )
141 140 adantr 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( M ... ( N - 1 ) ) = ( M ..^ N ) )
142 137 141 eleqtrd 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> k e. ( M ..^ N ) )
143 fzofzp1 
 |-  ( k e. ( M ..^ N ) -> ( k + 1 ) e. ( M ... N ) )
144 142 143 syl 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( k + 1 ) e. ( M ... N ) )
145 simpl 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ph )
146 145 144 jca 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( ph /\ ( k + 1 ) e. ( M ... N ) ) )
147 eleq1 
 |-  ( j = ( k + 1 ) -> ( j e. ( M ... N ) <-> ( k + 1 ) e. ( M ... N ) ) )
148 147 anbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ph /\ j e. ( M ... N ) ) <-> ( ph /\ ( k + 1 ) e. ( M ... N ) ) ) )
149 fveq2 
 |-  ( j = ( k + 1 ) -> ( F ` j ) = ( F ` ( k + 1 ) ) )
150 149 eleq1d 
 |-  ( j = ( k + 1 ) -> ( ( F ` j ) e. RR <-> ( F ` ( k + 1 ) ) e. RR ) )
151 148 150 imbi12d 
 |-  ( j = ( k + 1 ) -> ( ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR ) <-> ( ( ph /\ ( k + 1 ) e. ( M ... N ) ) -> ( F ` ( k + 1 ) ) e. RR ) ) )
152 eleq1 
 |-  ( k = j -> ( k e. ( M ... N ) <-> j e. ( M ... N ) ) )
153 152 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. ( M ... N ) ) <-> ( ph /\ j e. ( M ... N ) ) ) )
154 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
155 154 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. RR <-> ( F ` j ) e. RR ) )
156 153 155 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR ) ) )
157 156 1 chvarvv 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> ( F ` j ) e. RR )
158 151 157 vtoclg 
 |-  ( ( k + 1 ) e. ( M ... N ) -> ( ( ph /\ ( k + 1 ) e. ( M ... N ) ) -> ( F ` ( k + 1 ) ) e. RR ) )
159 144 146 158 sylc 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` ( k + 1 ) ) e. RR )
160 136 159 syldan 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( F ` ( k + 1 ) ) e. RR )
161 142 2 syldan 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )
162 136 161 syldan 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )
163 125 160 162 ltled 
 |-  ( ( ph /\ k e. ( ( I + 1 ) ... ( J - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
164 67 94 163 monoord 
 |-  ( ph -> ( F ` ( I + 1 ) ) <_ ( F ` J ) )
165 13 45 53 61 164 ltletrd 
 |-  ( ph -> ( F ` I ) < ( F ` J ) )