Metamath Proof Explorer


Theorem itgspltprt

Description: The S. integral splits on a given partition P . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgspltprt.1 φ M
itgspltprt.2 φ N M + 1
itgspltprt.3 φ P : M N
itgspltprt.4 φ i M ..^ N P i < P i + 1
itgspltprt.5 φ t P M P N A
itgspltprt.6 φ i M ..^ N t P i P i + 1 A 𝐿 1
Assertion itgspltprt φ P M P N A dt = i M ..^ N P i P i + 1 A dt

Proof

Step Hyp Ref Expression
1 itgspltprt.1 φ M
2 itgspltprt.2 φ N M + 1
3 itgspltprt.3 φ P : M N
4 itgspltprt.4 φ i M ..^ N P i < P i + 1
5 itgspltprt.5 φ t P M P N A
6 itgspltprt.6 φ i M ..^ N t P i P i + 1 A 𝐿 1
7 1 peano2zd φ M + 1
8 eluzelz N M + 1 N
9 2 8 syl φ N
10 7 9 9 3jca φ M + 1 N N
11 eluzle N M + 1 M + 1 N
12 2 11 syl φ M + 1 N
13 eluzelre N M + 1 N
14 2 13 syl φ N
15 14 leidd φ N N
16 10 12 15 jca32 φ M + 1 N N M + 1 N N N
17 elfz2 N M + 1 N M + 1 N N M + 1 N N N
18 16 17 sylibr φ N M + 1 N
19 fveq2 j = M + 1 P j = P M + 1
20 19 oveq2d j = M + 1 P M P j = P M P M + 1
21 20 itgeq1d j = M + 1 P M P j A dt = P M P M + 1 A dt
22 oveq2 j = M + 1 M ..^ j = M ..^ M + 1
23 22 sumeq1d j = M + 1 i M ..^ j P i P i + 1 A dt = i M ..^ M + 1 P i P i + 1 A dt
24 21 23 eqeq12d j = M + 1 P M P j A dt = i M ..^ j P i P i + 1 A dt P M P M + 1 A dt = i M ..^ M + 1 P i P i + 1 A dt
25 24 imbi2d j = M + 1 φ P M P j A dt = i M ..^ j P i P i + 1 A dt φ P M P M + 1 A dt = i M ..^ M + 1 P i P i + 1 A dt
26 fveq2 j = k P j = P k
27 26 oveq2d j = k P M P j = P M P k
28 27 itgeq1d j = k P M P j A dt = P M P k A dt
29 oveq2 j = k M ..^ j = M ..^ k
30 29 sumeq1d j = k i M ..^ j P i P i + 1 A dt = i M ..^ k P i P i + 1 A dt
31 28 30 eqeq12d j = k P M P j A dt = i M ..^ j P i P i + 1 A dt P M P k A dt = i M ..^ k P i P i + 1 A dt
32 31 imbi2d j = k φ P M P j A dt = i M ..^ j P i P i + 1 A dt φ P M P k A dt = i M ..^ k P i P i + 1 A dt
33 fveq2 j = k + 1 P j = P k + 1
34 33 oveq2d j = k + 1 P M P j = P M P k + 1
35 34 itgeq1d j = k + 1 P M P j A dt = P M P k + 1 A dt
36 oveq2 j = k + 1 M ..^ j = M ..^ k + 1
37 36 sumeq1d j = k + 1 i M ..^ j P i P i + 1 A dt = i M ..^ k + 1 P i P i + 1 A dt
38 35 37 eqeq12d j = k + 1 P M P j A dt = i M ..^ j P i P i + 1 A dt P M P k + 1 A dt = i M ..^ k + 1 P i P i + 1 A dt
39 38 imbi2d j = k + 1 φ P M P j A dt = i M ..^ j P i P i + 1 A dt φ P M P k + 1 A dt = i M ..^ k + 1 P i P i + 1 A dt
40 fveq2 j = N P j = P N
41 40 oveq2d j = N P M P j = P M P N
42 41 itgeq1d j = N P M P j A dt = P M P N A dt
43 oveq2 j = N M ..^ j = M ..^ N
44 43 sumeq1d j = N i M ..^ j P i P i + 1 A dt = i M ..^ N P i P i + 1 A dt
45 42 44 eqeq12d j = N P M P j A dt = i M ..^ j P i P i + 1 A dt P M P N A dt = i M ..^ N P i P i + 1 A dt
46 45 imbi2d j = N φ P M P j A dt = i M ..^ j P i P i + 1 A dt φ P M P N A dt = i M ..^ N P i P i + 1 A dt
47 1 adantl N M + 1 φ M
48 fzval3 M M M = M ..^ M + 1
49 47 48 syl N M + 1 φ M M = M ..^ M + 1
50 49 eqcomd N M + 1 φ M ..^ M + 1 = M M
51 50 sumeq1d N M + 1 φ i M ..^ M + 1 P i P i + 1 A dt = i = M M P i P i + 1 A dt
52 3 adantr φ t P M P M + 1 P : M N
53 1 zred φ M
54 1red φ 1
55 53 54 readdcld φ M + 1
56 53 ltp1d φ M < M + 1
57 53 55 14 56 12 ltletrd φ M < N
58 53 14 57 ltled φ M N
59 eluz M N N M M N
60 1 9 59 syl2anc φ N M M N
61 58 60 mpbird φ N M
62 eluzfz1 N M M M N
63 61 62 syl φ M M N
64 63 adantr φ t P M P M + 1 M M N
65 52 64 ffvelrnd φ t P M P M + 1 P M
66 elfz1 M N N M N N M N N N
67 1 9 66 syl2anc φ N M N N M N N N
68 9 58 15 67 mpbir3and φ N M N
69 3 68 ffvelrnd φ P N
70 69 adantr φ t P M P M + 1 P N
71 53 lep1d φ M M + 1
72 elfz1 M N M + 1 M N M + 1 M M + 1 M + 1 N
73 1 9 72 syl2anc φ M + 1 M N M + 1 M M + 1 M + 1 N
74 7 71 12 73 mpbir3and φ M + 1 M N
75 3 74 ffvelrnd φ P M + 1
76 75 adantr φ t P M P M + 1 P M + 1
77 simpr φ t P M P M + 1 t P M P M + 1
78 eliccre P M P M + 1 t P M P M + 1 t
79 65 76 77 78 syl3anc φ t P M P M + 1 t
80 3 63 ffvelrnd φ P M
81 80 rexrd φ P M *
82 81 adantr φ t P M P M + 1 P M *
83 76 rexrd φ t P M P M + 1 P M + 1 *
84 iccgelb P M * P M + 1 * t P M P M + 1 P M t
85 82 83 77 84 syl3anc φ t P M P M + 1 P M t
86 iccleub P M * P M + 1 * t P M P M + 1 t P M + 1
87 82 83 77 86 syl3anc φ t P M P M + 1 t P M + 1
88 3 adantr φ i M + 1 N P : M N
89 elfzelz i M + 1 N i
90 89 adantl φ i M + 1 N i
91 53 adantr φ i M + 1 N M
92 90 zred φ i M + 1 N i
93 55 adantr φ i M + 1 N M + 1
94 56 adantr φ i M + 1 N M < M + 1
95 elfzle1 i M + 1 N M + 1 i
96 95 adantl φ i M + 1 N M + 1 i
97 91 93 92 94 96 ltletrd φ i M + 1 N M < i
98 91 92 97 ltled φ i M + 1 N M i
99 elfzle2 i M + 1 N i N
100 99 adantl φ i M + 1 N i N
101 1 9 jca φ M N
102 101 adantr φ i M + 1 N M N
103 elfz1 M N i M N i M i i N
104 102 103 syl φ i M + 1 N i M N i M i i N
105 90 98 100 104 mpbir3and φ i M + 1 N i M N
106 88 105 ffvelrnd φ i M + 1 N P i
107 3 adantr φ i M + 1 N 1 P : M N
108 elfzelz i M + 1 N 1 i
109 108 adantl φ i M + 1 N 1 i
110 53 adantr φ i M + 1 N 1 M
111 109 zred φ i M + 1 N 1 i
112 55 adantr φ i M + 1 N 1 M + 1
113 56 adantr φ i M + 1 N 1 M < M + 1
114 elfzle1 i M + 1 N 1 M + 1 i
115 114 adantl φ i M + 1 N 1 M + 1 i
116 110 112 111 113 115 ltletrd φ i M + 1 N 1 M < i
117 110 111 116 ltled φ i M + 1 N 1 M i
118 14 adantr φ i M + 1 N 1 N
119 1red φ i M + 1 N 1 1
120 118 119 resubcld φ i M + 1 N 1 N 1
121 elfzle2 i M + 1 N 1 i N 1
122 121 adantl φ i M + 1 N 1 i N 1
123 118 ltm1d φ i M + 1 N 1 N 1 < N
124 111 120 118 122 123 lelttrd φ i M + 1 N 1 i < N
125 111 118 124 ltled φ i M + 1 N 1 i N
126 101 adantr φ i M + 1 N 1 M N
127 126 103 syl φ i M + 1 N 1 i M N i M i i N
128 109 117 125 127 mpbir3and φ i M + 1 N 1 i M N
129 107 128 ffvelrnd φ i M + 1 N 1 P i
130 109 peano2zd φ i M + 1 N 1 i + 1
131 111 119 readdcld φ i M + 1 N 1 i + 1
132 110 111 119 116 ltadd1dd φ i M + 1 N 1 M + 1 < i + 1
133 110 112 131 113 132 lttrd φ i M + 1 N 1 M < i + 1
134 110 131 133 ltled φ i M + 1 N 1 M i + 1
135 zltp1le i N i < N i + 1 N
136 108 9 135 syl2anr φ i M + 1 N 1 i < N i + 1 N
137 124 136 mpbid φ i M + 1 N 1 i + 1 N
138 elfz1 M N i + 1 M N i + 1 M i + 1 i + 1 N
139 126 138 syl φ i M + 1 N 1 i + 1 M N i + 1 M i + 1 i + 1 N
140 130 134 137 139 mpbir3and φ i M + 1 N 1 i + 1 M N
141 107 140 ffvelrnd φ i M + 1 N 1 P i + 1
142 eluz M i i M M i
143 1 108 142 syl2an φ i M + 1 N 1 i M M i
144 117 143 mpbird φ i M + 1 N 1 i M
145 9 adantr φ i M + 1 N 1 N
146 elfzo2 i M ..^ N i M N i < N
147 144 145 124 146 syl3anbrc φ i M + 1 N 1 i M ..^ N
148 147 4 syldan φ i M + 1 N 1 P i < P i + 1
149 129 141 148 ltled φ i M + 1 N 1 P i P i + 1
150 2 106 149 monoord φ P M + 1 P N
151 150 adantr φ t P M P M + 1 P M + 1 P N
152 79 76 70 87 151 letrd φ t P M P M + 1 t P N
153 65 70 79 85 152 eliccd φ t P M P M + 1 t P M P N
154 153 5 syldan φ t P M P M + 1 A
155 id φ φ
156 fzolb M M ..^ N M N M < N
157 1 9 57 156 syl3anbrc φ M M ..^ N
158 155 157 jca φ φ M M ..^ N
159 eleq1 i = M i M ..^ N M M ..^ N
160 159 anbi2d i = M φ i M ..^ N φ M M ..^ N
161 fveq2 i = M P i = P M
162 fvoveq1 i = M P i + 1 = P M + 1
163 161 162 oveq12d i = M P i P i + 1 = P M P M + 1
164 163 mpteq1d i = M t P i P i + 1 A = t P M P M + 1 A
165 164 eleq1d i = M t P i P i + 1 A 𝐿 1 t P M P M + 1 A 𝐿 1
166 160 165 imbi12d i = M φ i M ..^ N t P i P i + 1 A 𝐿 1 φ M M ..^ N t P M P M + 1 A 𝐿 1
167 166 6 vtoclg M φ M M ..^ N t P M P M + 1 A 𝐿 1
168 1 158 167 sylc φ t P M P M + 1 A 𝐿 1
169 154 168 itgcl φ P M P M + 1 A dt
170 163 itgeq1d i = M P i P i + 1 A dt = P M P M + 1 A dt
171 170 fsum1 M P M P M + 1 A dt i = M M P i P i + 1 A dt = P M P M + 1 A dt
172 1 169 171 syl2anc φ i = M M P i P i + 1 A dt = P M P M + 1 A dt
173 172 adantl N M + 1 φ i = M M P i P i + 1 A dt = P M P M + 1 A dt
174 51 173 eqtr2d N M + 1 φ P M P M + 1 A dt = i M ..^ M + 1 P i P i + 1 A dt
175 174 ex N M + 1 φ P M P M + 1 A dt = i M ..^ M + 1 P i P i + 1 A dt
176 simp3 k M + 1 ..^ N φ P M P k A dt = i M ..^ k P i P i + 1 A dt φ φ
177 simp1 k M + 1 ..^ N φ P M P k A dt = i M ..^ k P i P i + 1 A dt φ k M + 1 ..^ N
178 simp2 k M + 1 ..^ N φ P M P k A dt = i M ..^ k P i P i + 1 A dt φ φ P M P k A dt = i M ..^ k P i P i + 1 A dt
179 176 178 mpd k M + 1 ..^ N φ P M P k A dt = i M ..^ k P i P i + 1 A dt φ P M P k A dt = i M ..^ k P i P i + 1 A dt
180 53 adantr φ k M + 1 ..^ N M
181 elfzoelz k M + 1 ..^ N k
182 181 zred k M + 1 ..^ N k
183 182 adantl φ k M + 1 ..^ N k
184 55 adantr φ k M + 1 ..^ N M + 1
185 56 adantr φ k M + 1 ..^ N M < M + 1
186 elfzole1 k M + 1 ..^ N M + 1 k
187 186 adantl φ k M + 1 ..^ N M + 1 k
188 180 184 183 185 187 ltletrd φ k M + 1 ..^ N M < k
189 180 183 188 ltled φ k M + 1 ..^ N M k
190 eluz M k k M M k
191 1 181 190 syl2an φ k M + 1 ..^ N k M M k
192 189 191 mpbird φ k M + 1 ..^ N k M
193 simplll φ k M + 1 ..^ N i M k t P i P i + 1 φ
194 eliccxr t P i P i + 1 t *
195 194 adantl φ k M + 1 ..^ N i M k t P i P i + 1 t *
196 193 80 syl φ k M + 1 ..^ N i M k t P i P i + 1 P M
197 193 3 syl φ k M + 1 ..^ N i M k t P i P i + 1 P : M N
198 elfzelz i M k i
199 198 adantl φ k M + 1 ..^ N i M k i
200 elfzle1 i M k M i
201 200 adantl φ k M + 1 ..^ N i M k M i
202 199 zred φ k M + 1 ..^ N i M k i
203 14 ad2antrr φ k M + 1 ..^ N i M k N
204 183 adantr φ k M + 1 ..^ N i M k k
205 elfzle2 i M k i k
206 205 adantl φ k M + 1 ..^ N i M k i k
207 elfzolt2 k M + 1 ..^ N k < N
208 207 ad2antlr φ k M + 1 ..^ N i M k k < N
209 202 204 203 206 208 lelttrd φ k M + 1 ..^ N i M k i < N
210 202 203 209 ltled φ k M + 1 ..^ N i M k i N
211 101 ad2antrr φ k M + 1 ..^ N i M k M N
212 211 103 syl φ k M + 1 ..^ N i M k i M N i M i i N
213 199 201 210 212 mpbir3and φ k M + 1 ..^ N i M k i M N
214 213 adantr φ k M + 1 ..^ N i M k t P i P i + 1 i M N
215 197 214 ffvelrnd φ k M + 1 ..^ N i M k t P i P i + 1 P i
216 199 peano2zd φ k M + 1 ..^ N i M k i + 1
217 53 ad2antrr φ k M + 1 ..^ N i M k M
218 216 zred φ k M + 1 ..^ N i M k i + 1
219 53 adantr φ i M k M
220 198 zred i M k i
221 220 adantl φ i M k i
222 1red φ i M k 1
223 221 222 readdcld φ i M k i + 1
224 200 adantl φ i M k M i
225 221 ltp1d φ i M k i < i + 1
226 219 221 223 224 225 lelttrd φ i M k M < i + 1
227 226 adantlr φ k M + 1 ..^ N i M k M < i + 1
228 217 218 227 ltled φ k M + 1 ..^ N i M k M i + 1
229 9 198 anim12ci φ i M k i N
230 229 adantlr φ k M + 1 ..^ N i M k i N
231 230 135 syl φ k M + 1 ..^ N i M k i < N i + 1 N
232 209 231 mpbid φ k M + 1 ..^ N i M k i + 1 N
233 211 138 syl φ k M + 1 ..^ N i M k i + 1 M N i + 1 M i + 1 i + 1 N
234 216 228 232 233 mpbir3and φ k M + 1 ..^ N i M k i + 1 M N
235 234 adantr φ k M + 1 ..^ N i M k t P i P i + 1 i + 1 M N
236 197 235 ffvelrnd φ k M + 1 ..^ N i M k t P i P i + 1 P i + 1
237 simpr φ k M + 1 ..^ N i M k t P i P i + 1 t P i P i + 1
238 eliccre P i P i + 1 t P i P i + 1 t
239 215 236 237 238 syl3anc φ k M + 1 ..^ N i M k t P i P i + 1 t
240 elfzuz i M k i M
241 240 adantl φ k M + 1 ..^ N i M k i M
242 3 ad3antrrr φ k M + 1 ..^ N i M k j M i P : M N
243 elfzelz j M i j
244 243 adantl φ k M + 1 ..^ N i M k j M i j
245 elfzle1 j M i M j
246 245 adantl φ k M + 1 ..^ N i M k j M i M j
247 244 zred φ k M + 1 ..^ N i M k j M i j
248 203 adantr φ k M + 1 ..^ N i M k j M i N
249 202 adantr φ k M + 1 ..^ N i M k j M i i
250 elfzle2 j M i j i
251 250 adantl φ k M + 1 ..^ N i M k j M i j i
252 209 adantr φ k M + 1 ..^ N i M k j M i i < N
253 247 249 248 251 252 lelttrd φ k M + 1 ..^ N i M k j M i j < N
254 247 248 253 ltled φ k M + 1 ..^ N i M k j M i j N
255 211 adantr φ k M + 1 ..^ N i M k j M i M N
256 elfz1 M N j M N j M j j N
257 255 256 syl φ k M + 1 ..^ N i M k j M i j M N j M j j N
258 244 246 254 257 mpbir3and φ k M + 1 ..^ N i M k j M i j M N
259 242 258 ffvelrnd φ k M + 1 ..^ N i M k j M i P j
260 3 ad3antrrr φ k M + 1 ..^ N i M k j M i 1 P : M N
261 elfzelz j M i 1 j
262 261 adantl φ k M + 1 ..^ N i M k j M i 1 j
263 elfzle1 j M i 1 M j
264 263 adantl φ k M + 1 ..^ N i M k j M i 1 M j
265 262 zred φ k M + 1 ..^ N i M k j M i 1 j
266 203 adantr φ k M + 1 ..^ N i M k j M i 1 N
267 202 adantr φ k M + 1 ..^ N i M k j M i 1 i
268 1red φ k M + 1 ..^ N i M k j M i 1 1
269 267 268 resubcld φ k M + 1 ..^ N i M k j M i 1 i 1
270 elfzle2 j M i 1 j i 1
271 270 adantl φ k M + 1 ..^ N i M k j M i 1 j i 1
272 267 ltm1d φ k M + 1 ..^ N i M k j M i 1 i 1 < i
273 265 269 267 271 272 lelttrd φ k M + 1 ..^ N i M k j M i 1 j < i
274 209 adantr φ k M + 1 ..^ N i M k j M i 1 i < N
275 265 267 266 273 274 lttrd φ k M + 1 ..^ N i M k j M i 1 j < N
276 265 266 275 ltled φ k M + 1 ..^ N i M k j M i 1 j N
277 211 adantr φ k M + 1 ..^ N i M k j M i 1 M N
278 277 256 syl φ k M + 1 ..^ N i M k j M i 1 j M N j M j j N
279 262 264 276 278 mpbir3and φ k M + 1 ..^ N i M k j M i 1 j M N
280 260 279 ffvelrnd φ k M + 1 ..^ N i M k j M i 1 P j
281 262 peano2zd φ k M + 1 ..^ N i M k j M i 1 j + 1
282 180 ad2antrr φ k M + 1 ..^ N i M k j M i 1 M
283 265 268 readdcld φ k M + 1 ..^ N i M k j M i 1 j + 1
284 53 adantr φ j M i 1 M
285 261 zred j M i 1 j
286 285 adantl φ j M i 1 j
287 1red φ j M i 1 1
288 286 287 readdcld φ j M i 1 j + 1
289 263 adantl φ j M i 1 M j
290 286 ltp1d φ j M i 1 j < j + 1
291 284 286 288 289 290 lelttrd φ j M i 1 M < j + 1
292 291 ad4ant14 φ k M + 1 ..^ N i M k j M i 1 M < j + 1
293 282 283 292 ltled φ k M + 1 ..^ N i M k j M i 1 M j + 1
294 zltp1le j i j < i j + 1 i
295 261 199 294 syl2anr φ k M + 1 ..^ N i M k j M i 1 j < i j + 1 i
296 273 295 mpbid φ k M + 1 ..^ N i M k j M i 1 j + 1 i
297 283 267 266 296 274 lelttrd φ k M + 1 ..^ N i M k j M i 1 j + 1 < N
298 283 266 297 ltled φ k M + 1 ..^ N i M k j M i 1 j + 1 N
299 elfz1 M N j + 1 M N j + 1 M j + 1 j + 1 N
300 277 299 syl φ k M + 1 ..^ N i M k j M i 1 j + 1 M N j + 1 M j + 1 j + 1 N
301 281 293 298 300 mpbir3and φ k M + 1 ..^ N i M k j M i 1 j + 1 M N
302 260 301 ffvelrnd φ k M + 1 ..^ N i M k j M i 1 P j + 1
303 simplll φ k M + 1 ..^ N i M k j M i 1 φ
304 elfzuz j M i 1 j M
305 304 adantl φ k M + 1 ..^ N i M k j M i 1 j M
306 303 9 syl φ k M + 1 ..^ N i M k j M i 1 N
307 elfzo2 j M ..^ N j M N j < N
308 305 306 275 307 syl3anbrc φ k M + 1 ..^ N i M k j M i 1 j M ..^ N
309 eleq1 i = j i M ..^ N j M ..^ N
310 309 anbi2d i = j φ i M ..^ N φ j M ..^ N
311 fveq2 i = j P i = P j
312 fvoveq1 i = j P i + 1 = P j + 1
313 311 312 breq12d i = j P i < P i + 1 P j < P j + 1
314 310 313 imbi12d i = j φ i M ..^ N P i < P i + 1 φ j M ..^ N P j < P j + 1
315 314 4 chvarvv φ j M ..^ N P j < P j + 1
316 303 308 315 syl2anc φ k M + 1 ..^ N i M k j M i 1 P j < P j + 1
317 280 302 316 ltled φ k M + 1 ..^ N i M k j M i 1 P j P j + 1
318 241 259 317 monoord φ k M + 1 ..^ N i M k P M P i
319 318 adantr φ k M + 1 ..^ N i M k t P i P i + 1 P M P i
320 215 rexrd φ k M + 1 ..^ N i M k t P i P i + 1 P i *
321 236 rexrd φ k M + 1 ..^ N i M k t P i P i + 1 P i + 1 *
322 iccgelb P i * P i + 1 * t P i P i + 1 P i t
323 320 321 237 322 syl3anc φ k M + 1 ..^ N i M k t P i P i + 1 P i t
324 196 215 239 319 323 letrd φ k M + 1 ..^ N i M k t P i P i + 1 P M t
325 193 69 syl φ k M + 1 ..^ N i M k t P i P i + 1 P N
326 iccleub P i * P i + 1 * t P i P i + 1 t P i + 1
327 320 321 237 326 syl3anc φ k M + 1 ..^ N i M k t P i P i + 1 t P i + 1
328 9 ad2antrr φ k M + 1 ..^ N i M k N
329 eluz i + 1 N N i + 1 i + 1 N
330 216 328 329 syl2anc φ k M + 1 ..^ N i M k N i + 1 i + 1 N
331 232 330 mpbird φ k M + 1 ..^ N i M k N i + 1
332 331 adantr φ k M + 1 ..^ N i M k t P i P i + 1 N i + 1
333 3 ad3antrrr φ k M + 1 ..^ N i M k j i + 1 N P : M N
334 elfzelz j i + 1 N j
335 334 adantl φ k M + 1 ..^ N i M k j i + 1 N j
336 elfzel1 i M k M
337 336 zred i M k M
338 337 adantr i M k j i + 1 N M
339 334 zred j i + 1 N j
340 339 adantl i M k j i + 1 N j
341 220 adantr i M k j i + 1 N i
342 1red i M k j i + 1 N 1
343 341 342 readdcld i M k j i + 1 N i + 1
344 200 adantr i M k j i + 1 N M i
345 341 ltp1d i M k j i + 1 N i < i + 1
346 338 341 343 344 345 lelttrd i M k j i + 1 N M < i + 1
347 elfzle1 j i + 1 N i + 1 j
348 347 adantl i M k j i + 1 N i + 1 j
349 338 343 340 346 348 ltletrd i M k j i + 1 N M < j
350 338 340 349 ltled i M k j i + 1 N M j
351 350 adantll φ k M + 1 ..^ N i M k j i + 1 N M j
352 elfzle2 j i + 1 N j N
353 352 adantl φ k M + 1 ..^ N i M k j i + 1 N j N
354 211 adantr φ k M + 1 ..^ N i M k j i + 1 N M N
355 354 256 syl φ k M + 1 ..^ N i M k j i + 1 N j M N j M j j N
356 335 351 353 355 mpbir3and φ k M + 1 ..^ N i M k j i + 1 N j M N
357 333 356 ffvelrnd φ k M + 1 ..^ N i M k j i + 1 N P j
358 357 adantlr φ k M + 1 ..^ N i M k t P i P i + 1 j i + 1 N P j
359 simplll φ k M + 1 ..^ N i M k j i + 1 N 1 φ
360 simplr φ k M + 1 ..^ N i M k j i + 1 N 1 i M k
361 simpr φ k M + 1 ..^ N i M k j i + 1 N 1 j i + 1 N 1
362 3 3ad2ant1 φ i M k j i + 1 N 1 P : M N
363 elfzelz j i + 1 N 1 j
364 363 3ad2ant3 φ i M k j i + 1 N 1 j
365 53 3ad2ant1 φ i M k j i + 1 N 1 M
366 364 zred φ i M k j i + 1 N 1 j
367 223 3adant3 φ i M k j i + 1 N 1 i + 1
368 226 3adant3 φ i M k j i + 1 N 1 M < i + 1
369 elfzle1 j i + 1 N 1 i + 1 j
370 369 3ad2ant3 φ i M k j i + 1 N 1 i + 1 j
371 365 367 366 368 370 ltletrd φ i M k j i + 1 N 1 M < j
372 365 366 371 ltled φ i M k j i + 1 N 1 M j
373 363 adantl φ j i + 1 N 1 j
374 373 zred φ j i + 1 N 1 j
375 14 adantr φ j i + 1 N 1 N
376 1red φ j i + 1 N 1 1
377 375 376 resubcld φ j i + 1 N 1 N 1
378 elfzle2 j i + 1 N 1 j N 1
379 378 adantl φ j i + 1 N 1 j N 1
380 375 ltm1d φ j i + 1 N 1 N 1 < N
381 374 377 375 379 380 lelttrd φ j i + 1 N 1 j < N
382 374 375 381 ltled φ j i + 1 N 1 j N
383 382 3adant2 φ i M k j i + 1 N 1 j N
384 101 3ad2ant1 φ i M k j i + 1 N 1 M N
385 384 256 syl φ i M k j i + 1 N 1 j M N j M j j N
386 364 372 383 385 mpbir3and φ i M k j i + 1 N 1 j M N
387 362 386 ffvelrnd φ i M k j i + 1 N 1 P j
388 364 peano2zd φ i M k j i + 1 N 1 j + 1
389 388 zred φ i M k j i + 1 N 1 j + 1
390 220 3ad2ant2 φ i M k j i + 1 N 1 i
391 1red φ i M k j i + 1 N 1 1
392 225 3adant3 φ i M k j i + 1 N 1 i < i + 1
393 390 367 366 392 370 ltletrd φ i M k j i + 1 N 1 i < j
394 390 366 393 ltled φ i M k j i + 1 N 1 i j
395 390 366 391 394 leadd1dd φ i M k j i + 1 N 1 i + 1 j + 1
396 365 367 389 368 395 ltletrd φ i M k j i + 1 N 1 M < j + 1
397 365 389 396 ltled φ i M k j i + 1 N 1 M j + 1
398 zltp1le j N j < N j + 1 N
399 363 9 398 syl2anr φ j i + 1 N 1 j < N j + 1 N
400 381 399 mpbid φ j i + 1 N 1 j + 1 N
401 400 3adant2 φ i M k j i + 1 N 1 j + 1 N
402 384 299 syl φ i M k j i + 1 N 1 j + 1 M N j + 1 M j + 1 j + 1 N
403 388 397 401 402 mpbir3and φ i M k j i + 1 N 1 j + 1 M N
404 362 403 ffvelrnd φ i M k j i + 1 N 1 P j + 1
405 simp1 φ i M k j i + 1 N 1 φ
406 1 3ad2ant1 φ i M k j i + 1 N 1 M
407 eluz M j j M M j
408 406 364 407 syl2anc φ i M k j i + 1 N 1 j M M j
409 372 408 mpbird φ i M k j i + 1 N 1 j M
410 9 3ad2ant1 φ i M k j i + 1 N 1 N
411 381 3adant2 φ i M k j i + 1 N 1 j < N
412 409 410 411 307 syl3anbrc φ i M k j i + 1 N 1 j M ..^ N
413 405 412 315 syl2anc φ i M k j i + 1 N 1 P j < P j + 1
414 387 404 413 ltled φ i M k j i + 1 N 1 P j P j + 1
415 359 360 361 414 syl3anc φ k M + 1 ..^ N i M k j i + 1 N 1 P j P j + 1
416 415 adantlr φ k M + 1 ..^ N i M k t P i P i + 1 j i + 1 N 1 P j P j + 1
417 332 358 416 monoord φ k M + 1 ..^ N i M k t P i P i + 1 P i + 1 P N
418 239 236 325 327 417 letrd φ k M + 1 ..^ N i M k t P i P i + 1 t P N
419 69 rexrd φ P N *
420 81 419 jca φ P M * P N *
421 193 420 syl φ k M + 1 ..^ N i M k t P i P i + 1 P M * P N *
422 elicc1 P M * P N * t P M P N t * P M t t P N
423 421 422 syl φ k M + 1 ..^ N i M k t P i P i + 1 t P M P N t * P M t t P N
424 195 324 418 423 mpbir3and φ k M + 1 ..^ N i M k t P i P i + 1 t P M P N
425 193 424 5 syl2anc φ k M + 1 ..^ N i M k t P i P i + 1 A
426 simpll φ k M + 1 ..^ N i M k φ
427 241 328 209 146 syl3anbrc φ k M + 1 ..^ N i M k i M ..^ N
428 426 427 6 syl2anc φ k M + 1 ..^ N i M k t P i P i + 1 A 𝐿 1
429 425 428 itgcl φ k M + 1 ..^ N i M k P i P i + 1 A dt
430 fveq2 i = k P i = P k
431 fvoveq1 i = k P i + 1 = P k + 1
432 430 431 oveq12d i = k P i P i + 1 = P k P k + 1
433 432 itgeq1d i = k P i P i + 1 A dt = P k P k + 1 A dt
434 192 429 433 fzosump1 φ k M + 1 ..^ N i M ..^ k + 1 P i P i + 1 A dt = i M ..^ k P i P i + 1 A dt + P k P k + 1 A dt
435 434 3adant3 φ k M + 1 ..^ N P M P k A dt = i M ..^ k P i P i + 1 A dt i M ..^ k + 1 P i P i + 1 A dt = i M ..^ k P i P i + 1 A dt + P k P k + 1 A dt
436 oveq1 P M P k A dt = i M ..^ k P i P i + 1 A dt P M P k A dt + P k P k + 1 A dt = i M ..^ k P i P i + 1 A dt + P k P k + 1 A dt
437 436 eqcomd P M P k A dt = i M ..^ k P i P i + 1 A dt i M ..^ k P i P i + 1 A dt + P k P k + 1 A dt = P M P k A dt + P k P k + 1 A dt
438 437 3ad2ant3 φ k M + 1 ..^ N P M P k A dt = i M ..^ k P i P i + 1 A dt i M ..^ k P i P i + 1 A dt + P k P k + 1 A dt = P M P k A dt + P k P k + 1 A dt
439 80 adantr φ k M + 1 ..^ N P M
440 3 adantr φ k M + 1 ..^ N P : M N
441 181 adantl φ k M + 1 ..^ N k
442 441 peano2zd φ k M + 1 ..^ N k + 1
443 442 zred φ k M + 1 ..^ N k + 1
444 183 ltp1d φ k M + 1 ..^ N k < k + 1
445 180 183 443 188 444 lttrd φ k M + 1 ..^ N M < k + 1
446 180 443 445 ltled φ k M + 1 ..^ N M k + 1
447 207 adantl φ k M + 1 ..^ N k < N
448 zltp1le k N k < N k + 1 N
449 181 9 448 syl2anr φ k M + 1 ..^ N k < N k + 1 N
450 447 449 mpbid φ k M + 1 ..^ N k + 1 N
451 101 adantr φ k M + 1 ..^ N M N
452 elfz1 M N k + 1 M N k + 1 M k + 1 k + 1 N
453 451 452 syl φ k M + 1 ..^ N k + 1 M N k + 1 M k + 1 k + 1 N
454 442 446 450 453 mpbir3and φ k M + 1 ..^ N k + 1 M N
455 440 454 ffvelrnd φ k M + 1 ..^ N P k + 1
456 14 adantr φ k M + 1 ..^ N N
457 183 456 447 ltled φ k M + 1 ..^ N k N
458 elfz1 M N k M N k M k k N
459 451 458 syl φ k M + 1 ..^ N k M N k M k k N
460 441 189 457 459 mpbir3and φ k M + 1 ..^ N k M N
461 440 460 ffvelrnd φ k M + 1 ..^ N P k
462 461 rexrd φ k M + 1 ..^ N P k *
463 3 ad2antrr φ k M + 1 ..^ N i M k P : M N
464 463 213 ffvelrnd φ k M + 1 ..^ N i M k P i
465 3 ad2antrr φ k M + 1 ..^ N i M k 1 P : M N
466 elfzelz i M k 1 i
467 466 adantl φ k M + 1 ..^ N i M k 1 i
468 elfzle1 i M k 1 M i
469 468 adantl φ k M + 1 ..^ N i M k 1 M i
470 467 zred φ k M + 1 ..^ N i M k 1 i
471 14 ad2antrr φ k M + 1 ..^ N i M k 1 N
472 183 adantr φ k M + 1 ..^ N i M k 1 k
473 1red φ k M + 1 ..^ N i M k 1 1
474 472 473 resubcld φ k M + 1 ..^ N i M k 1 k 1
475 elfzle2 i M k 1 i k 1
476 475 adantl φ k M + 1 ..^ N i M k 1 i k 1
477 472 ltm1d φ k M + 1 ..^ N i M k 1 k 1 < k
478 470 474 472 476 477 lelttrd φ k M + 1 ..^ N i M k 1 i < k
479 447 adantr φ k M + 1 ..^ N i M k 1 k < N
480 470 472 471 478 479 lttrd φ k M + 1 ..^ N i M k 1 i < N
481 470 471 480 ltled φ k M + 1 ..^ N i M k 1 i N
482 101 ad2antrr φ k M + 1 ..^ N i M k 1 M N
483 482 103 syl φ k M + 1 ..^ N i M k 1 i M N i M i i N
484 467 469 481 483 mpbir3and φ k M + 1 ..^ N i M k 1 i M N
485 465 484 ffvelrnd φ k M + 1 ..^ N i M k 1 P i
486 467 peano2zd φ k M + 1 ..^ N i M k 1 i + 1
487 53 ad2antrr φ k M + 1 ..^ N i M k 1 M
488 470 473 readdcld φ k M + 1 ..^ N i M k 1 i + 1
489 470 ltp1d φ k M + 1 ..^ N i M k 1 i < i + 1
490 487 470 488 469 489 lelttrd φ k M + 1 ..^ N i M k 1 M < i + 1
491 487 488 490 ltled φ k M + 1 ..^ N i M k 1 M i + 1
492 zltp1le i k i < k i + 1 k
493 466 441 492 syl2anr φ k M + 1 ..^ N i M k 1 i < k i + 1 k
494 478 493 mpbid φ k M + 1 ..^ N i M k 1 i + 1 k
495 488 472 471 494 479 lelttrd φ k M + 1 ..^ N i M k 1 i + 1 < N
496 488 471 495 ltled φ k M + 1 ..^ N i M k 1 i + 1 N
497 482 138 syl φ k M + 1 ..^ N i M k 1 i + 1 M N i + 1 M i + 1 i + 1 N
498 486 491 496 497 mpbir3and φ k M + 1 ..^ N i M k 1 i + 1 M N
499 465 498 ffvelrnd φ k M + 1 ..^ N i M k 1 P i + 1
500 simpll φ k M + 1 ..^ N i M k 1 φ
501 elfzuz i M k 1 i M
502 501 adantl φ k M + 1 ..^ N i M k 1 i M
503 9 ad2antrr φ k M + 1 ..^ N i M k 1 N
504 502 503 480 146 syl3anbrc φ k M + 1 ..^ N i M k 1 i M ..^ N
505 500 504 4 syl2anc φ k M + 1 ..^ N i M k 1 P i < P i + 1
506 485 499 505 ltled φ k M + 1 ..^ N i M k 1 P i P i + 1
507 192 464 506 monoord φ k M + 1 ..^ N P M P k
508 9 adantr φ k M + 1 ..^ N N
509 elfzo2 k M ..^ N k M N k < N
510 192 508 447 509 syl3anbrc φ k M + 1 ..^ N k M ..^ N
511 eleq1 i = k i M ..^ N k M ..^ N
512 511 anbi2d i = k φ i M ..^ N φ k M ..^ N
513 430 431 breq12d i = k P i < P i + 1 P k < P k + 1
514 512 513 imbi12d i = k φ i M ..^ N P i < P i + 1 φ k M ..^ N P k < P k + 1
515 514 4 chvarvv φ k M ..^ N P k < P k + 1
516 510 515 syldan φ k M + 1 ..^ N P k < P k + 1
517 461 455 516 ltled φ k M + 1 ..^ N P k P k + 1
518 81 adantr φ k M + 1 ..^ N P M *
519 455 rexrd φ k M + 1 ..^ N P k + 1 *
520 elicc1 P M * P k + 1 * P k P M P k + 1 P k * P M P k P k P k + 1
521 518 519 520 syl2anc φ k M + 1 ..^ N P k P M P k + 1 P k * P M P k P k P k + 1
522 462 507 517 521 mpbir3and φ k M + 1 ..^ N P k P M P k + 1
523 simpll φ k M + 1 ..^ N t P M P k + 1 φ
524 eliccxr t P M P k + 1 t *
525 524 adantl φ k M + 1 ..^ N t P M P k + 1 t *
526 81 ad2antrr φ k M + 1 ..^ N t P M P k + 1 P M *
527 519 adantr φ k M + 1 ..^ N t P M P k + 1 P k + 1 *
528 simpr φ k M + 1 ..^ N t P M P k + 1 t P M P k + 1
529 iccgelb P M * P k + 1 * t P M P k + 1 P M t
530 526 527 528 529 syl3anc φ k M + 1 ..^ N t P M P k + 1 P M t
531 80 ad2antrr φ k M + 1 ..^ N t P M P k + 1 P M
532 455 adantr φ k M + 1 ..^ N t P M P k + 1 P k + 1
533 eliccre P M P k + 1 t P M P k + 1 t
534 531 532 528 533 syl3anc φ k M + 1 ..^ N t P M P k + 1 t
535 69 ad2antrr φ k M + 1 ..^ N t P M P k + 1 P N
536 iccleub P M * P k + 1 * t P M P k + 1 t P k + 1
537 526 527 528 536 syl3anc φ k M + 1 ..^ N t P M P k + 1 t P k + 1
538 eluz2 N k + 1 k + 1 N k + 1 N
539 442 508 450 538 syl3anbrc φ k M + 1 ..^ N N k + 1
540 3 ad2antrr φ k M + 1 ..^ N i k + 1 N P : M N
541 1 ad2antrr φ k M + 1 ..^ N i k + 1 N M
542 9 ad2antrr φ k M + 1 ..^ N i k + 1 N N
543 elfzelz i k + 1 N i
544 543 adantl φ k M + 1 ..^ N i k + 1 N i
545 541 542 544 3jca φ k M + 1 ..^ N i k + 1 N M N i
546 53 ad2antrr φ k M + 1 ..^ N i k + 1 N M
547 544 zred φ k M + 1 ..^ N i k + 1 N i
548 183 adantr φ k M + 1 ..^ N i k + 1 N k
549 188 adantr φ k M + 1 ..^ N i k + 1 N M < k
550 182 adantr k M + 1 ..^ N i k + 1 N k
551 1red k M + 1 ..^ N i k + 1 N 1
552 550 551 readdcld k M + 1 ..^ N i k + 1 N k + 1
553 543 zred i k + 1 N i
554 553 adantl k M + 1 ..^ N i k + 1 N i
555 550 ltp1d k M + 1 ..^ N i k + 1 N k < k + 1
556 elfzle1 i k + 1 N k + 1 i
557 556 adantl k M + 1 ..^ N i k + 1 N k + 1 i
558 550 552 554 555 557 ltletrd k M + 1 ..^ N i k + 1 N k < i
559 558 adantll φ k M + 1 ..^ N i k + 1 N k < i
560 546 548 547 549 559 lttrd φ k M + 1 ..^ N i k + 1 N M < i
561 546 547 560 ltled φ k M + 1 ..^ N i k + 1 N M i
562 elfzle2 i k + 1 N i N
563 562 adantl φ k M + 1 ..^ N i k + 1 N i N
564 545 561 563 jca32 φ k M + 1 ..^ N i k + 1 N M N i M i i N
565 elfz2 i M N M N i M i i N
566 564 565 sylibr φ k M + 1 ..^ N i k + 1 N i M N
567 540 566 ffvelrnd φ k M + 1 ..^ N i k + 1 N P i
568 3 ad2antrr φ k M + 1 ..^ N i k + 1 N 1 P : M N
569 1 ad2antrr φ k M + 1 ..^ N i k + 1 N 1 M
570 9 ad2antrr φ k M + 1 ..^ N i k + 1 N 1 N
571 elfzelz i k + 1 N 1 i
572 571 adantl φ k M + 1 ..^ N i k + 1 N 1 i
573 569 570 572 3jca φ k M + 1 ..^ N i k + 1 N 1 M N i
574 53 ad2antrr φ k M + 1 ..^ N i k + 1 N 1 M
575 572 zred φ k M + 1 ..^ N i k + 1 N 1 i
576 183 adantr φ k M + 1 ..^ N i k + 1 N 1 k
577 188 adantr φ k M + 1 ..^ N i k + 1 N 1 M < k
578 182 adantr k M + 1 ..^ N i k + 1 N 1 k
579 1red k M + 1 ..^ N i k + 1 N 1 1
580 578 579 readdcld k M + 1 ..^ N i k + 1 N 1 k + 1
581 571 zred i k + 1 N 1 i
582 581 adantl k M + 1 ..^ N i k + 1 N 1 i
583 578 ltp1d k M + 1 ..^ N i k + 1 N 1 k < k + 1
584 elfzle1 i k + 1 N 1 k + 1 i
585 584 adantl k M + 1 ..^ N i k + 1 N 1 k + 1 i
586 578 580 582 583 585 ltletrd k M + 1 ..^ N i k + 1 N 1 k < i
587 586 adantll φ k M + 1 ..^ N i k + 1 N 1 k < i
588 574 576 575 577 587 lttrd φ k M + 1 ..^ N i k + 1 N 1 M < i
589 574 575 588 ltled φ k M + 1 ..^ N i k + 1 N 1 M i
590 581 adantl φ i k + 1 N 1 i
591 14 adantr φ i k + 1 N 1 N
592 1red φ i k + 1 N 1 1
593 591 592 resubcld φ i k + 1 N 1 N 1
594 elfzle2 i k + 1 N 1 i N 1
595 594 adantl φ i k + 1 N 1 i N 1
596 591 ltm1d φ i k + 1 N 1 N 1 < N
597 590 593 591 595 596 lelttrd φ i k + 1 N 1 i < N
598 590 591 597 ltled φ i k + 1 N 1 i N
599 598 adantlr φ k M + 1 ..^ N i k + 1 N 1 i N
600 573 589 599 jca32 φ k M + 1 ..^ N i k + 1 N 1 M N i M i i N
601 600 565 sylibr φ k M + 1 ..^ N i k + 1 N 1 i M N
602 568 601 ffvelrnd φ k M + 1 ..^ N i k + 1 N 1 P i
603 572 peano2zd φ k M + 1 ..^ N i k + 1 N 1 i + 1
604 569 570 603 3jca φ k M + 1 ..^ N i k + 1 N 1 M N i + 1
605 603 zred φ k M + 1 ..^ N i k + 1 N 1 i + 1
606 575 ltp1d φ k M + 1 ..^ N i k + 1 N 1 i < i + 1
607 576 575 605 587 606 lttrd φ k M + 1 ..^ N i k + 1 N 1 k < i + 1
608 574 576 605 577 607 lttrd φ k M + 1 ..^ N i k + 1 N 1 M < i + 1
609 574 605 608 ltled φ k M + 1 ..^ N i k + 1 N 1 M i + 1
610 597 adantlr φ k M + 1 ..^ N i k + 1 N 1 i < N
611 571 508 135 syl2anr φ k M + 1 ..^ N i k + 1 N 1 i < N i + 1 N
612 610 611 mpbid φ k M + 1 ..^ N i k + 1 N 1 i + 1 N
613 604 609 612 jca32 φ k M + 1 ..^ N i k + 1 N 1 M N i + 1 M i + 1 i + 1 N
614 elfz2 i + 1 M N M N i + 1 M i + 1 i + 1 N
615 613 614 sylibr φ k M + 1 ..^ N i k + 1 N 1 i + 1 M N
616 568 615 ffvelrnd φ k M + 1 ..^ N i k + 1 N 1 P i + 1
617 simpll φ k M + 1 ..^ N i k + 1 N 1 φ
618 eluz2 i M M i M i
619 569 572 589 618 syl3anbrc φ k M + 1 ..^ N i k + 1 N 1 i M
620 619 570 610 146 syl3anbrc φ k M + 1 ..^ N i k + 1 N 1 i M ..^ N
621 617 620 4 syl2anc φ k M + 1 ..^ N i k + 1 N 1 P i < P i + 1
622 602 616 621 ltled φ k M + 1 ..^ N i k + 1 N 1 P i P i + 1
623 539 567 622 monoord φ k M + 1 ..^ N P k + 1 P N
624 623 adantr φ k M + 1 ..^ N t P M P k + 1 P k + 1 P N
625 534 532 535 537 624 letrd φ k M + 1 ..^ N t P M P k + 1 t P N
626 420 ad2antrr φ k M + 1 ..^ N t P M P k + 1 P M * P N *
627 626 422 syl φ k M + 1 ..^ N t P M P k + 1 t P M P N t * P M t t P N
628 525 530 625 627 mpbir3and φ k M + 1 ..^ N t P M P k + 1 t P M P N
629 523 628 5 syl2anc φ k M + 1 ..^ N t P M P k + 1 A
630 nfv t φ k M + 1 ..^ N
631 1 adantr φ k M + 1 ..^ N M
632 elfzouz k M + 1 ..^ N k M + 1
633 632 adantl φ k M + 1 ..^ N k M + 1
634 simpll φ k M + 1 ..^ N i M ..^ k φ
635 elfzouz i M ..^ k i M
636 635 adantl φ k M + 1 ..^ N i M ..^ k i M
637 9 ad2antrr φ k M + 1 ..^ N i M ..^ k N
638 elfzoelz i M ..^ k i
639 638 zred i M ..^ k i
640 639 adantl φ k M + 1 ..^ N i M ..^ k i
641 183 adantr φ k M + 1 ..^ N i M ..^ k k
642 14 ad2antrr φ k M + 1 ..^ N i M ..^ k N
643 elfzolt2 i M ..^ k i < k
644 643 adantl φ k M + 1 ..^ N i M ..^ k i < k
645 447 adantr φ k M + 1 ..^ N i M ..^ k k < N
646 640 641 642 644 645 lttrd φ k M + 1 ..^ N i M ..^ k i < N
647 636 637 646 146 syl3anbrc φ k M + 1 ..^ N i M ..^ k i M ..^ N
648 634 647 4 syl2anc φ k M + 1 ..^ N i M ..^ k P i < P i + 1
649 simpll φ k M + 1 ..^ N t P M P k φ
650 80 ad2antrr φ k M + 1 ..^ N t P M P k P M
651 69 ad2antrr φ k M + 1 ..^ N t P M P k P N
652 461 adantr φ k M + 1 ..^ N t P M P k P k
653 simpr φ k M + 1 ..^ N t P M P k t P M P k
654 eliccre P M P k t P M P k t
655 650 652 653 654 syl3anc φ k M + 1 ..^ N t P M P k t
656 81 ad2antrr φ k M + 1 ..^ N t P M P k P M *
657 462 adantr φ k M + 1 ..^ N t P M P k P k *
658 iccgelb P M * P k * t P M P k P M t
659 656 657 653 658 syl3anc φ k M + 1 ..^ N t P M P k P M t
660 iccleub P M * P k * t P M P k t P k
661 656 657 653 660 syl3anc φ k M + 1 ..^ N t P M P k t P k
662 elfzouz2 k M + 1 ..^ N N k
663 662 adantl φ k M + 1 ..^ N N k
664 3 ad2antrr φ k M + 1 ..^ N i k N P : M N
665 1 ad2antrr φ k M + 1 ..^ N i k N M
666 9 ad2antrr φ k M + 1 ..^ N i k N N
667 elfzelz i k N i
668 667 adantl φ k M + 1 ..^ N i k N i
669 665 666 668 3jca φ k M + 1 ..^ N i k N M N i
670 53 ad2antrr φ k M + 1 ..^ N i k N M
671 668 zred φ k M + 1 ..^ N i k N i
672 183 adantr φ k M + 1 ..^ N i k N k
673 188 adantr φ k M + 1 ..^ N i k N M < k
674 elfzle1 i k N k i
675 674 adantl φ k M + 1 ..^ N i k N k i
676 670 672 671 673 675 ltletrd φ k M + 1 ..^ N i k N M < i
677 670 671 676 ltled φ k M + 1 ..^ N i k N M i
678 elfzle2 i k N i N
679 678 adantl φ k M + 1 ..^ N i k N i N
680 669 677 679 jca32 φ k M + 1 ..^ N i k N M N i M i i N
681 680 565 sylibr φ k M + 1 ..^ N i k N i M N
682 664 681 ffvelrnd φ k M + 1 ..^ N i k N P i
683 3 ad2antrr φ k M + 1 ..^ N i k N 1 P : M N
684 1 ad2antrr φ k M + 1 ..^ N i k N 1 M
685 9 ad2antrr φ k M + 1 ..^ N i k N 1 N
686 elfzelz i k N 1 i
687 686 adantl φ k M + 1 ..^ N i k N 1 i
688 684 685 687 3jca φ k M + 1 ..^ N i k N 1 M N i
689 53 ad2antrr φ k M + 1 ..^ N i k N 1 M
690 687 zred φ k M + 1 ..^ N i k N 1 i
691 183 adantr φ k M + 1 ..^ N i k N 1 k
692 188 adantr φ k M + 1 ..^ N i k N 1 M < k
693 elfzle1 i k N 1 k i
694 693 adantl φ k M + 1 ..^ N i k N 1 k i
695 689 691 690 692 694 ltletrd φ k M + 1 ..^ N i k N 1 M < i
696 689 690 695 ltled φ k M + 1 ..^ N i k N 1 M i
697 686 zred i k N 1 i
698 697 adantl φ i k N 1 i
699 14 adantr φ i k N 1 N
700 1red φ i k N 1 1
701 699 700 resubcld φ i k N 1 N 1
702 elfzle2 i k N 1 i N 1
703 702 adantl φ i k N 1 i N 1
704 699 ltm1d φ i k N 1 N 1 < N
705 698 701 699 703 704 lelttrd φ i k N 1 i < N
706 698 699 705 ltled φ i k N 1 i N
707 706 adantlr φ k M + 1 ..^ N i k N 1 i N
708 688 696 707 jca32 φ k M + 1 ..^ N i k N 1 M N i M i i N
709 708 565 sylibr φ k M + 1 ..^ N i k N 1 i M N
710 683 709 ffvelrnd φ k M + 1 ..^ N i k N 1 P i
711 687 peano2zd φ k M + 1 ..^ N i k N 1 i + 1
712 684 685 711 3jca φ k M + 1 ..^ N i k N 1 M N i + 1
713 711 zred φ k M + 1 ..^ N i k N 1 i + 1
714 690 ltp1d φ k M + 1 ..^ N i k N 1 i < i + 1
715 689 690 713 696 714 lelttrd φ k M + 1 ..^ N i k N 1 M < i + 1
716 689 713 715 ltled φ k M + 1 ..^ N i k N 1 M i + 1
717 686 9 135 syl2anr φ i k N 1 i < N i + 1 N
718 705 717 mpbid φ i k N 1 i + 1 N
719 718 adantlr φ k M + 1 ..^ N i k N 1 i + 1 N
720 712 716 719 jca32 φ k M + 1 ..^ N i k N 1 M N i + 1 M i + 1 i + 1 N
721 720 614 sylibr φ k M + 1 ..^ N i k N 1 i + 1 M N
722 683 721 ffvelrnd φ k M + 1 ..^ N i k N 1 P i + 1
723 simpll φ k M + 1 ..^ N i k N 1 φ
724 684 687 696 618 syl3anbrc φ k M + 1 ..^ N i k N 1 i M
725 705 adantlr φ k M + 1 ..^ N i k N 1 i < N
726 724 685 725 146 syl3anbrc φ k M + 1 ..^ N i k N 1 i M ..^ N
727 723 726 4 syl2anc φ k M + 1 ..^ N i k N 1 P i < P i + 1
728 710 722 727 ltled φ k M + 1 ..^ N i k N 1 P i P i + 1
729 663 682 728 monoord φ k M + 1 ..^ N P k P N
730 729 adantr φ k M + 1 ..^ N t P M P