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