Metamath Proof Explorer


Theorem fourierdlem64

Description: The partition V is finer than Q , when Q is moved on the same interval where V lies. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem64.t T = B A
fourierdlem64.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem64.m φ M
fourierdlem64.q φ Q P M
fourierdlem64.c φ C
fourierdlem64.d φ D
fourierdlem64.cltd φ C < D
fourierdlem64.h H = C D y C D | k y + k T ran Q
fourierdlem64.n N = H 1
fourierdlem64.v V = ι f | f Isom < , < 0 N H
fourierdlem64.j φ J 0 ..^ N
fourierdlem64.l L = sup k | Q 0 + k T V J <
fourierdlem64.i I = sup j 0 ..^ M | Q j + L T V J <
Assertion fourierdlem64 φ I 0 ..^ M L i 0 ..^ M l V J V J + 1 Q i + l T Q i + 1 + l T

Proof

Step Hyp Ref Expression
1 fourierdlem64.t T = B A
2 fourierdlem64.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
3 fourierdlem64.m φ M
4 fourierdlem64.q φ Q P M
5 fourierdlem64.c φ C
6 fourierdlem64.d φ D
7 fourierdlem64.cltd φ C < D
8 fourierdlem64.h H = C D y C D | k y + k T ran Q
9 fourierdlem64.n N = H 1
10 fourierdlem64.v V = ι f | f Isom < , < 0 N H
11 fourierdlem64.j φ J 0 ..^ N
12 fourierdlem64.l L = sup k | Q 0 + k T V J <
13 fourierdlem64.i I = sup j 0 ..^ M | Q j + L T V J <
14 ssrab2 j 0 ..^ M | Q j + L T V J 0 ..^ M
15 fzossfz 0 ..^ M 0 M
16 fzssz 0 M
17 15 16 sstri 0 ..^ M
18 14 17 sstri j 0 ..^ M | Q j + L T V J
19 18 a1i φ j 0 ..^ M | Q j + L T V J
20 0zd φ 0
21 3 nnzd φ M
22 3 nngt0d φ 0 < M
23 fzolb 0 0 ..^ M 0 M 0 < M
24 20 21 22 23 syl3anbrc φ 0 0 ..^ M
25 ssrab2 k | Q 0 + k T V J
26 25 a1i φ k | Q 0 + k T V J
27 prssi C D C D
28 5 6 27 syl2anc φ C D
29 ssrab2 y C D | k y + k T ran Q C D
30 29 a1i φ y C D | k y + k T ran Q C D
31 5 6 iccssred φ C D
32 30 31 sstrd φ y C D | k y + k T ran Q
33 28 32 unssd φ C D y C D | k y + k T ran Q
34 8 33 eqsstrid φ H
35 eqid m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
36 1 2 3 4 5 6 7 35 8 9 10 fourierdlem54 φ N V m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1 N V Isom < , < 0 N H
37 36 simprd φ V Isom < , < 0 N H
38 isof1o V Isom < , < 0 N H V : 0 N 1-1 onto H
39 f1of V : 0 N 1-1 onto H V : 0 N H
40 37 38 39 3syl φ V : 0 N H
41 elfzofz J 0 ..^ N J 0 N
42 11 41 syl φ J 0 N
43 40 42 ffvelrnd φ V J H
44 34 43 sseldd φ V J
45 2 fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
46 3 45 syl φ Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
47 4 46 mpbid φ Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
48 47 simpld φ Q 0 M
49 elmapi Q 0 M Q : 0 M
50 48 49 syl φ Q : 0 M
51 3 nnnn0d φ M 0
52 nn0uz 0 = 0
53 51 52 eleqtrdi φ M 0
54 eluzfz1 M 0 0 0 M
55 53 54 syl φ 0 0 M
56 50 55 ffvelrnd φ Q 0
57 44 56 resubcld φ V J Q 0
58 2 3 4 fourierdlem11 φ A B A < B
59 58 simp2d φ B
60 58 simp1d φ A
61 59 60 resubcld φ B A
62 1 61 eqeltrid φ T
63 58 simp3d φ A < B
64 60 59 posdifd φ A < B 0 < B A
65 63 64 mpbid φ 0 < B A
66 65 1 breqtrrdi φ 0 < T
67 66 gt0ne0d φ T 0
68 57 62 67 redivcld φ V J Q 0 T
69 btwnz V J Q 0 T k k < V J Q 0 T z V J Q 0 T < z
70 68 69 syl φ k k < V J Q 0 T z V J Q 0 T < z
71 70 simpld φ k k < V J Q 0 T
72 zre k k
73 56 ad2antrr φ k k < V J Q 0 T Q 0
74 simplr φ k k < V J Q 0 T k
75 62 ad2antrr φ k k < V J Q 0 T T
76 74 75 remulcld φ k k < V J Q 0 T k T
77 73 76 readdcld φ k k < V J Q 0 T Q 0 + k T
78 44 ad2antrr φ k k < V J Q 0 T V J
79 simpr φ k k < V J Q 0 T k < V J Q 0 T
80 57 ad2antrr φ k k < V J Q 0 T V J Q 0
81 62 66 elrpd φ T +
82 81 ad2antrr φ k k < V J Q 0 T T +
83 74 80 82 ltmuldivd φ k k < V J Q 0 T k T < V J Q 0 k < V J Q 0 T
84 79 83 mpbird φ k k < V J Q 0 T k T < V J Q 0
85 56 adantr φ k Q 0
86 simpr φ k k
87 62 adantr φ k T
88 86 87 remulcld φ k k T
89 44 adantr φ k V J
90 85 88 89 ltaddsub2d φ k Q 0 + k T < V J k T < V J Q 0
91 90 adantr φ k k < V J Q 0 T Q 0 + k T < V J k T < V J Q 0
92 84 91 mpbird φ k k < V J Q 0 T Q 0 + k T < V J
93 77 78 92 ltled φ k k < V J Q 0 T Q 0 + k T V J
94 93 ex φ k k < V J Q 0 T Q 0 + k T V J
95 72 94 sylan2 φ k k < V J Q 0 T Q 0 + k T V J
96 95 reximdva φ k k < V J Q 0 T k Q 0 + k T V J
97 71 96 mpd φ k Q 0 + k T V J
98 rabn0 k | Q 0 + k T V J k Q 0 + k T V J
99 97 98 sylibr φ k | Q 0 + k T V J
100 simpl φ j k | Q 0 + k T V J φ
101 26 sselda φ j k | Q 0 + k T V J j
102 oveq1 k = j k T = j T
103 102 oveq2d k = j Q 0 + k T = Q 0 + j T
104 103 breq1d k = j Q 0 + k T V J Q 0 + j T V J
105 104 elrab j k | Q 0 + k T V J j Q 0 + j T V J
106 105 simprbi j k | Q 0 + k T V J Q 0 + j T V J
107 106 adantl φ j k | Q 0 + k T V J Q 0 + j T V J
108 zre j j
109 simpr φ j Q 0 + j T V J Q 0 + j T V J
110 56 ad2antrr φ j Q 0 + j T V J Q 0
111 simpr φ j j
112 62 adantr φ j T
113 111 112 remulcld φ j j T
114 113 adantr φ j Q 0 + j T V J j T
115 44 ad2antrr φ j Q 0 + j T V J V J
116 110 114 115 leaddsub2d φ j Q 0 + j T V J Q 0 + j T V J j T V J Q 0
117 109 116 mpbid φ j Q 0 + j T V J j T V J Q 0
118 simplr φ j Q 0 + j T V J j
119 57 ad2antrr φ j Q 0 + j T V J V J Q 0
120 81 ad2antrr φ j Q 0 + j T V J T +
121 118 119 120 lemuldivd φ j Q 0 + j T V J j T V J Q 0 j V J Q 0 T
122 117 121 mpbid φ j Q 0 + j T V J j V J Q 0 T
123 108 122 sylanl2 φ j Q 0 + j T V J j V J Q 0 T
124 100 101 107 123 syl21anc φ j k | Q 0 + k T V J j V J Q 0 T
125 124 ralrimiva φ j k | Q 0 + k T V J j V J Q 0 T
126 breq2 b = V J Q 0 T j b j V J Q 0 T
127 126 ralbidv b = V J Q 0 T j k | Q 0 + k T V J j b j k | Q 0 + k T V J j V J Q 0 T
128 127 rspcev V J Q 0 T j k | Q 0 + k T V J j V J Q 0 T b j k | Q 0 + k T V J j b
129 68 125 128 syl2anc φ b j k | Q 0 + k T V J j b
130 suprzcl k | Q 0 + k T V J k | Q 0 + k T V J b j k | Q 0 + k T V J j b sup k | Q 0 + k T V J < k | Q 0 + k T V J
131 26 99 129 130 syl3anc φ sup k | Q 0 + k T V J < k | Q 0 + k T V J
132 12 131 eqeltrid φ L k | Q 0 + k T V J
133 oveq1 k = L k T = L T
134 133 oveq2d k = L Q 0 + k T = Q 0 + L T
135 134 breq1d k = L Q 0 + k T V J Q 0 + L T V J
136 135 elrab L k | Q 0 + k T V J L Q 0 + L T V J
137 132 136 sylib φ L Q 0 + L T V J
138 137 simprd φ Q 0 + L T V J
139 fveq2 j = 0 Q j = Q 0
140 139 oveq1d j = 0 Q j + L T = Q 0 + L T
141 140 breq1d j = 0 Q j + L T V J Q 0 + L T V J
142 141 elrab 0 j 0 ..^ M | Q j + L T V J 0 0 ..^ M Q 0 + L T V J
143 24 138 142 sylanbrc φ 0 j 0 ..^ M | Q j + L T V J
144 ne0i 0 j 0 ..^ M | Q j + L T V J j 0 ..^ M | Q j + L T V J
145 143 144 syl φ j 0 ..^ M | Q j + L T V J
146 3 nnred φ M
147 14 a1i φ j 0 ..^ M | Q j + L T V J 0 ..^ M
148 147 sselda φ k j 0 ..^ M | Q j + L T V J k 0 ..^ M
149 elfzoelz k 0 ..^ M k
150 149 zred k 0 ..^ M k
151 150 adantl φ k 0 ..^ M k
152 146 adantr φ k 0 ..^ M M
153 elfzolt2 k 0 ..^ M k < M
154 153 adantl φ k 0 ..^ M k < M
155 151 152 154 ltled φ k 0 ..^ M k M
156 148 155 syldan φ k j 0 ..^ M | Q j + L T V J k M
157 156 ralrimiva φ k j 0 ..^ M | Q j + L T V J k M
158 breq2 b = M k b k M
159 158 ralbidv b = M k j 0 ..^ M | Q j + L T V J k b k j 0 ..^ M | Q j + L T V J k M
160 159 rspcev M k j 0 ..^ M | Q j + L T V J k M b k j 0 ..^ M | Q j + L T V J k b
161 146 157 160 syl2anc φ b k j 0 ..^ M | Q j + L T V J k b
162 suprzcl j 0 ..^ M | Q j + L T V J j 0 ..^ M | Q j + L T V J b k j 0 ..^ M | Q j + L T V J k b sup j 0 ..^ M | Q j + L T V J < j 0 ..^ M | Q j + L T V J
163 19 145 161 162 syl3anc φ sup j 0 ..^ M | Q j + L T V J < j 0 ..^ M | Q j + L T V J
164 14 163 sseldi φ sup j 0 ..^ M | Q j + L T V J < 0 ..^ M
165 13 164 eqeltrid φ I 0 ..^ M
166 25 131 sseldi φ sup k | Q 0 + k T V J <
167 12 166 eqeltrid φ L
168 15 165 sseldi φ I 0 M
169 50 168 ffvelrnd φ Q I
170 167 zred φ L
171 170 62 remulcld φ L T
172 169 171 readdcld φ Q I + L T
173 172 rexrd φ Q I + L T *
174 173 adantr φ x V J V J + 1 Q I + L T *
175 fzofzp1 I 0 ..^ M I + 1 0 M
176 165 175 syl φ I + 1 0 M
177 50 176 ffvelrnd φ Q I + 1
178 177 171 readdcld φ Q I + 1 + L T
179 178 rexrd φ Q I + 1 + L T *
180 179 adantr φ x V J V J + 1 Q I + 1 + L T *
181 elioore x V J V J + 1 x
182 181 adantl φ x V J V J + 1 x
183 172 adantr φ x V J V J + 1 Q I + L T
184 44 adantr φ x V J V J + 1 V J
185 13 163 eqeltrid φ I j 0 ..^ M | Q j + L T V J
186 fveq2 j = I Q j = Q I
187 186 oveq1d j = I Q j + L T = Q I + L T
188 187 breq1d j = I Q j + L T V J Q I + L T V J
189 188 elrab I j 0 ..^ M | Q j + L T V J I 0 ..^ M Q I + L T V J
190 185 189 sylib φ I 0 ..^ M Q I + L T V J
191 190 simprd φ Q I + L T V J
192 191 adantr φ x V J V J + 1 Q I + L T V J
193 184 rexrd φ x V J V J + 1 V J *
194 fzofzp1 J 0 ..^ N J + 1 0 N
195 11 194 syl φ J + 1 0 N
196 40 195 ffvelrnd φ V J + 1 H
197 34 196 sseldd φ V J + 1
198 197 rexrd φ V J + 1 *
199 198 adantr φ x V J V J + 1 V J + 1 *
200 simpr φ x V J V J + 1 x V J V J + 1
201 ioogtlb V J * V J + 1 * x V J V J + 1 V J < x
202 193 199 200 201 syl3anc φ x V J V J + 1 V J < x
203 183 184 182 192 202 lelttrd φ x V J V J + 1 Q I + L T < x
204 zssre
205 25 204 sstri k | Q 0 + k T V J
206 205 a1i φ I = M 1 Q I + 1 + L T V J k | Q 0 + k T V J
207 99 ad2antrr φ I = M 1 Q I + 1 + L T V J k | Q 0 + k T V J
208 129 ad2antrr φ I = M 1 Q I + 1 + L T V J b j k | Q 0 + k T V J j b
209 167 peano2zd φ L + 1
210 209 ad2antrr φ I = M 1 Q I + 1 + L T V J L + 1
211 oveq1 I = M 1 I + 1 = M - 1 + 1
212 146 recnd φ M
213 1cnd φ 1
214 212 213 npcand φ M - 1 + 1 = M
215 211 214 sylan9eqr φ I = M 1 I + 1 = M
216 215 fveq2d φ I = M 1 Q I + 1 = Q M
217 47 simprd φ Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
218 217 simpld φ Q 0 = A Q M = B
219 218 simprd φ Q M = B
220 219 adantr φ I = M 1 Q M = B
221 59 recnd φ B
222 60 recnd φ A
223 221 222 npcand φ B - A + A = B
224 223 eqcomd φ B = B - A + A
225 1 eqcomi B A = T
226 225 a1i φ B A = T
227 226 oveq1d φ B - A + A = T + A
228 218 simpld φ Q 0 = A
229 228 eqcomd φ A = Q 0
230 229 oveq2d φ T + A = T + Q 0
231 224 227 230 3eqtrd φ B = T + Q 0
232 231 adantr φ I = M 1 B = T + Q 0
233 216 220 232 3eqtrd φ I = M 1 Q I + 1 = T + Q 0
234 62 recnd φ T
235 228 222 eqeltrd φ Q 0
236 234 235 addcomd φ T + Q 0 = Q 0 + T
237 236 adantr φ I = M 1 T + Q 0 = Q 0 + T
238 233 237 eqtrd φ I = M 1 Q I + 1 = Q 0 + T
239 238 oveq1d φ I = M 1 Q I + 1 + L T = Q 0 + T + L T
240 171 recnd φ L T
241 235 234 240 addassd φ Q 0 + T + L T = Q 0 + T + L T
242 234 mulid2d φ 1 T = T
243 242 234 eqeltrd φ 1 T
244 243 240 addcomd φ 1 T + L T = L T + 1 T
245 242 eqcomd φ T = 1 T
246 245 oveq1d φ T + L T = 1 T + L T
247 170 recnd φ L
248 247 213 234 adddird φ L + 1 T = L T + 1 T
249 244 246 248 3eqtr4d φ T + L T = L + 1 T
250 249 oveq2d φ Q 0 + T + L T = Q 0 + L + 1 T
251 241 250 eqtrd φ Q 0 + T + L T = Q 0 + L + 1 T
252 251 adantr φ I = M 1 Q 0 + T + L T = Q 0 + L + 1 T
253 239 252 eqtr2d φ I = M 1 Q 0 + L + 1 T = Q I + 1 + L T
254 253 adantr φ I = M 1 Q I + 1 + L T V J Q 0 + L + 1 T = Q I + 1 + L T
255 simpr φ I = M 1 Q I + 1 + L T V J Q I + 1 + L T V J
256 254 255 eqbrtrd φ I = M 1 Q I + 1 + L T V J Q 0 + L + 1 T V J
257 oveq1 k = L + 1 k T = L + 1 T
258 257 oveq2d k = L + 1 Q 0 + k T = Q 0 + L + 1 T
259 258 breq1d k = L + 1 Q 0 + k T V J Q 0 + L + 1 T V J
260 259 elrab L + 1 k | Q 0 + k T V J L + 1 Q 0 + L + 1 T V J
261 210 256 260 sylanbrc φ I = M 1 Q I + 1 + L T V J L + 1 k | Q 0 + k T V J
262 suprub k | Q 0 + k T V J k | Q 0 + k T V J b j k | Q 0 + k T V J j b L + 1 k | Q 0 + k T V J L + 1 sup k | Q 0 + k T V J <
263 206 207 208 261 262 syl31anc φ I = M 1 Q I + 1 + L T V J L + 1 sup k | Q 0 + k T V J <
264 263 12 breqtrrdi φ I = M 1 Q I + 1 + L T V J L + 1 L
265 170 ltp1d φ L < L + 1
266 peano2re L L + 1
267 170 266 syl φ L + 1
268 170 267 ltnled φ L < L + 1 ¬ L + 1 L
269 265 268 mpbid φ ¬ L + 1 L
270 269 ad2antrr φ I = M 1 Q I + 1 + L T V J ¬ L + 1 L
271 264 270 pm2.65da φ I = M 1 ¬ Q I + 1 + L T V J
272 17 165 sseldi φ I
273 272 zred φ I
274 273 adantr φ ¬ I = M 1 I
275 peano2rem M M 1
276 146 275 syl φ M 1
277 276 adantr φ ¬ I = M 1 M 1
278 elfzolt2 I 0 ..^ M I < M
279 elfzoelz I 0 ..^ M I
280 elfzoel2 I 0 ..^ M M
281 zltlem1 I M I < M I M 1
282 279 280 281 syl2anc I 0 ..^ M I < M I M 1
283 278 282 mpbid I 0 ..^ M I M 1
284 165 283 syl φ I M 1
285 284 adantr φ ¬ I = M 1 I M 1
286 neqne ¬ I = M 1 I M 1
287 286 necomd ¬ I = M 1 M 1 I
288 287 adantl φ ¬ I = M 1 M 1 I
289 274 277 285 288 leneltd φ ¬ I = M 1 I < M 1
290 18 204 sstri j 0 ..^ M | Q j + L T V J
291 290 a1i φ I < M 1 Q I + 1 + L T V J j 0 ..^ M | Q j + L T V J
292 145 ad2antrr φ I < M 1 Q I + 1 + L T V J j 0 ..^ M | Q j + L T V J
293 161 ad2antrr φ I < M 1 Q I + 1 + L T V J b k j 0 ..^ M | Q j + L T V J k b
294 176 adantr φ I < M 1 I + 1 0 M
295 273 adantr φ I < M 1 I
296 276 adantr φ I < M 1 M 1
297 1red φ I < M 1 1
298 simpr φ I < M 1 I < M 1
299 295 296 297 298 ltadd1dd φ I < M 1 I + 1 < M - 1 + 1
300 214 adantr φ I < M 1 M - 1 + 1 = M
301 299 300 breqtrd φ I < M 1 I + 1 < M
302 elfzfzo I + 1 0 ..^ M I + 1 0 M I + 1 < M
303 294 301 302 sylanbrc φ I < M 1 I + 1 0 ..^ M
304 303 anim1i φ I < M 1 Q I + 1 + L T V J I + 1 0 ..^ M Q I + 1 + L T V J
305 fveq2 j = I + 1 Q j = Q I + 1
306 305 oveq1d j = I + 1 Q j + L T = Q I + 1 + L T
307 306 breq1d j = I + 1 Q j + L T V J Q I + 1 + L T V J
308 307 elrab I + 1 j 0 ..^ M | Q j + L T V J I + 1 0 ..^ M Q I + 1 + L T V J
309 304 308 sylibr φ I < M 1 Q I + 1 + L T V J I + 1 j 0 ..^ M | Q j + L T V J
310 suprub j 0 ..^ M | Q j + L T V J j 0 ..^ M | Q j + L T V J b k j 0 ..^ M | Q j + L T V J k b I + 1 j 0 ..^ M | Q j + L T V J I + 1 sup j 0 ..^ M | Q j + L T V J <
311 291 292 293 309 310 syl31anc φ I < M 1 Q I + 1 + L T V J I + 1 sup j 0 ..^ M | Q j + L T V J <
312 311 13 breqtrrdi φ I < M 1 Q I + 1 + L T V J I + 1 I
313 273 ltp1d φ I < I + 1
314 peano2re I I + 1
315 273 314 syl φ I + 1
316 273 315 ltnled φ I < I + 1 ¬ I + 1 I
317 313 316 mpbid φ ¬ I + 1 I
318 317 ad2antrr φ I < M 1 Q I + 1 + L T V J ¬ I + 1 I
319 312 318 pm2.65da φ I < M 1 ¬ Q I + 1 + L T V J
320 289 319 syldan φ ¬ I = M 1 ¬ Q I + 1 + L T V J
321 271 320 pm2.61dan φ ¬ Q I + 1 + L T V J
322 44 178 ltnled φ V J < Q I + 1 + L T ¬ Q I + 1 + L T V J
323 321 322 mpbird φ V J < Q I + 1 + L T
324 197 adantr φ D Q I + 1 + L T V J + 1
325 6 adantr φ D Q I + 1 + L T D
326 178 adantr φ D Q I + 1 + L T Q I + 1 + L T
327 5 rexrd φ C *
328 6 rexrd φ D *
329 5 6 7 ltled φ C D
330 lbicc2 C * D * C D C C D
331 327 328 329 330 syl3anc φ C C D
332 ubicc2 C * D * C D D C D
333 327 328 329 332 syl3anc φ D C D
334 331 333 jca φ C C D D C D
335 prssg C D C C D D C D C D C D
336 5 6 335 syl2anc φ C C D D C D C D C D
337 334 336 mpbid φ C D C D
338 337 30 unssd φ C D y C D | k y + k T ran Q C D
339 8 338 eqsstrid φ H C D
340 339 196 sseldd φ V J + 1 C D
341 iccleub C * D * V J + 1 C D V J + 1 D
342 327 328 340 341 syl3anc φ V J + 1 D
343 342 adantr φ D Q I + 1 + L T V J + 1 D
344 simpr φ D Q I + 1 + L T D Q I + 1 + L T
345 324 325 326 343 344 letrd φ D Q I + 1 + L T V J + 1 Q I + 1 + L T
346 345 adantlr φ V J < Q I + 1 + L T D Q I + 1 + L T V J + 1 Q I + 1 + L T
347 simpr φ ¬ D Q I + 1 + L T ¬ D Q I + 1 + L T
348 178 adantr φ ¬ D Q I + 1 + L T Q I + 1 + L T
349 6 adantr φ ¬ D Q I + 1 + L T D
350 348 349 ltnled φ ¬ D Q I + 1 + L T Q I + 1 + L T < D ¬ D Q I + 1 + L T
351 347 350 mpbird φ ¬ D Q I + 1 + L T Q I + 1 + L T < D
352 351 adantlr φ V J < Q I + 1 + L T ¬ D Q I + 1 + L T Q I + 1 + L T < D
353 simpll φ V J < Q I + 1 + L T Q I + 1 + L T < D ¬ V J + 1 Q I + 1 + L T φ V J < Q I + 1 + L T
354 simpr φ ¬ V J + 1 Q I + 1 + L T ¬ V J + 1 Q I + 1 + L T
355 178 adantr φ ¬ V J + 1 Q I + 1 + L T Q I + 1 + L T
356 197 adantr φ ¬ V J + 1 Q I + 1 + L T V J + 1
357 355 356 ltnled φ ¬ V J + 1 Q I + 1 + L T Q I + 1 + L T < V J + 1 ¬ V J + 1 Q I + 1 + L T
358 354 357 mpbird φ ¬ V J + 1 Q I + 1 + L T Q I + 1 + L T < V J + 1
359 358 ad4ant14 φ V J < Q I + 1 + L T Q I + 1 + L T < D ¬ V J + 1 Q I + 1 + L T Q I + 1 + L T < V J + 1
360 5 ad2antrr φ V J < Q I + 1 + L T Q I + 1 + L T < D C
361 6 ad2antrr φ V J < Q I + 1 + L T Q I + 1 + L T < D D
362 178 ad2antrr φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T
363 5 adantr φ V J < Q I + 1 + L T C
364 178 adantr φ V J < Q I + 1 + L T Q I + 1 + L T
365 44 adantr φ V J < Q I + 1 + L T V J
366 339 43 sseldd φ V J C D
367 iccgelb C * D * V J C D C V J
368 327 328 366 367 syl3anc φ C V J
369 368 adantr φ V J < Q I + 1 + L T C V J
370 simpr φ V J < Q I + 1 + L T V J < Q I + 1 + L T
371 363 365 364 369 370 lelttrd φ V J < Q I + 1 + L T C < Q I + 1 + L T
372 363 364 371 ltled φ V J < Q I + 1 + L T C Q I + 1 + L T
373 372 adantr φ V J < Q I + 1 + L T Q I + 1 + L T < D C Q I + 1 + L T
374 178 adantr φ Q I + 1 + L T < D Q I + 1 + L T
375 6 adantr φ Q I + 1 + L T < D D
376 simpr φ Q I + 1 + L T < D Q I + 1 + L T < D
377 374 375 376 ltled φ Q I + 1 + L T < D Q I + 1 + L T D
378 377 adantlr φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T D
379 360 361 362 373 378 eliccd φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T C D
380 167 znegcld φ L
381 247 234 mulneg1d φ L T = L T
382 381 oveq2d φ Q I + 1 + L T + L T = Q I + 1 + L T + L T
383 178 recnd φ Q I + 1 + L T
384 383 240 negsubd φ Q I + 1 + L T + L T = Q I + 1 + L T - L T
385 177 recnd φ Q I + 1
386 385 240 pncand φ Q I + 1 + L T - L T = Q I + 1
387 382 384 386 3eqtrd φ Q I + 1 + L T + L T = Q I + 1
388 ffn Q : 0 M Q Fn 0 M
389 50 388 syl φ Q Fn 0 M
390 fnfvelrn Q Fn 0 M I + 1 0 M Q I + 1 ran Q
391 389 176 390 syl2anc φ Q I + 1 ran Q
392 387 391 eqeltrd φ Q I + 1 + L T + L T ran Q
393 oveq1 k = L k T = L T
394 393 oveq2d k = L Q I + 1 + L T + k T = Q I + 1 + L T + L T
395 394 eleq1d k = L Q I + 1 + L T + k T ran Q Q I + 1 + L T + L T ran Q
396 395 rspcev L Q I + 1 + L T + L T ran Q k Q I + 1 + L T + k T ran Q
397 380 392 396 syl2anc φ k Q I + 1 + L T + k T ran Q
398 397 ad2antrr φ V J < Q I + 1 + L T Q I + 1 + L T < D k Q I + 1 + L T + k T ran Q
399 oveq1 y = Q I + 1 + L T y + k T = Q I + 1 + L T + k T
400 399 eleq1d y = Q I + 1 + L T y + k T ran Q Q I + 1 + L T + k T ran Q
401 400 rexbidv y = Q I + 1 + L T k y + k T ran Q k Q I + 1 + L T + k T ran Q
402 401 elrab Q I + 1 + L T y C D | k y + k T ran Q Q I + 1 + L T C D k Q I + 1 + L T + k T ran Q
403 379 398 402 sylanbrc φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T y C D | k y + k T ran Q
404 elun2 Q I + 1 + L T y C D | k y + k T ran Q Q I + 1 + L T C D y C D | k y + k T ran Q
405 403 404 syl φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T C D y C D | k y + k T ran Q
406 8 eqcomi C D y C D | k y + k T ran Q = H
407 405 406 eleqtrdi φ V J < Q I + 1 + L T Q I + 1 + L T < D Q I + 1 + L T H
408 407 adantr φ V J < Q I + 1 + L T Q I + 1 + L T < D ¬ V J + 1 Q I + 1 + L T Q I + 1 + L T H
409 f1ofo V : 0 N 1-1 onto H V : 0 N onto H
410 37 38 409 3syl φ V : 0 N onto H
411 foelrn V : 0 N onto H Q I + 1 + L T H j 0 N Q I + 1 + L T = V j
412 410 411 sylan φ Q I + 1 + L T H j 0 N Q I + 1 + L T = V j
413 id Q I + 1 + L T = V j Q I + 1 + L T = V j
414 413 eqcomd Q I + 1 + L T = V j V j = Q I + 1 + L T
415 414 a1i φ Q I + 1 + L T H Q I + 1 + L T = V j V j = Q I + 1 + L T
416 415 reximdv φ Q I + 1 + L T H j 0 N Q I + 1 + L T = V j j 0 N V j = Q I + 1 + L T
417 412 416 mpd φ Q I + 1 + L T H j 0 N V j = Q I + 1 + L T
418 417 ad4ant14 φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 Q I + 1 + L T H j 0 N V j = Q I + 1 + L T
419 simpl V J < Q I + 1 + L T V j = Q I + 1 + L T V J < Q I + 1 + L T
420 413 eqcoms V j = Q I + 1 + L T Q I + 1 + L T = V j
421 420 adantl V J < Q I + 1 + L T V j = Q I + 1 + L T Q I + 1 + L T = V j
422 419 421 breqtrd V J < Q I + 1 + L T V j = Q I + 1 + L T V J < V j
423 422 adantll φ V J < Q I + 1 + L T V j = Q I + 1 + L T V J < V j
424 423 adantlr φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T V J < V j
425 37 ad3antrrr φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T V Isom < , < 0 N H
426 42 ad3antrrr φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T J 0 N
427 simplr φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T j 0 N
428 isorel V Isom < , < 0 N H J 0 N j 0 N J < j V J < V j
429 425 426 427 428 syl12anc φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T J < j V J < V j
430 424 429 mpbird φ V J < Q I + 1 + L T j 0 N V j = Q I + 1 + L T J < j
431 430 adantllr φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T J < j
432 simpr Q I + 1 + L T < V J + 1 V j = Q I + 1 + L T V j = Q I + 1 + L T
433 simpl Q I + 1 + L T < V J + 1 V j = Q I + 1 + L T Q I + 1 + L T < V J + 1
434 432 433 eqbrtrd Q I + 1 + L T < V J + 1 V j = Q I + 1 + L T V j < V J + 1
435 434 adantll φ Q I + 1 + L T < V J + 1 V j = Q I + 1 + L T V j < V J + 1
436 435 adantlr φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T V j < V J + 1
437 37 ad3antrrr φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T V Isom < , < 0 N H
438 simplr φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T j 0 N
439 195 ad3antrrr φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T J + 1 0 N
440 isorel V Isom < , < 0 N H j 0 N J + 1 0 N j < J + 1 V j < V J + 1
441 437 438 439 440 syl12anc φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T j < J + 1 V j < V J + 1
442 436 441 mpbird φ Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T j < J + 1
443 442 adantl3r φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T j < J + 1
444 431 443 jca φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T J < j j < J + 1
445 444 ex φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 j 0 N V j = Q I + 1 + L T J < j j < J + 1
446 445 adantlr φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 Q I + 1 + L T H j 0 N V j = Q I + 1 + L T J < j j < J + 1
447 446 reximdva φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 Q I + 1 + L T H j 0 N V j = Q I + 1 + L T j 0 N J < j j < J + 1
448 418 447 mpd φ V J < Q I + 1 + L T Q I + 1 + L T < V J + 1 Q I + 1 + L T H j 0 N J < j j < J + 1
449 353 359 408 448 syl21anc φ V J < Q I + 1 + L T Q I + 1 + L T < D ¬ V J + 1 Q I + 1 + L T j 0 N J < j j < J + 1
450 elfzelz j 0 N j
451 450 ad2antlr φ j 0 N J < j j < J + 1 j
452 elfzelz J 0 N J
453 42 452 syl φ J
454 453 ad2antrr φ j 0 N J < j j < J + 1 J
455 simprl φ j 0 N J < j j < J + 1 J < j
456 simprr φ j 0 N J < j j < J + 1 j < J + 1
457 btwnnz J J < j j < J + 1 ¬ j
458 454 455 456 457 syl3anc φ j 0 N J < j j < J + 1 ¬ j
459 451 458 pm2.65da φ j 0 N ¬ J < j j < J + 1
460 459 nrexdv φ ¬ j 0 N J < j j < J + 1
461 460 ad3antrrr φ V J < Q I + 1 + L T Q I + 1 + L T < D ¬ V J + 1 Q I + 1 + L T ¬ j 0 N J < j j < J + 1
462 449 461 condan φ V J < Q I + 1 + L T Q I + 1 + L T < D V J + 1 Q I + 1 + L T
463 352 462 syldan φ V J < Q I + 1 + L T ¬ D Q I + 1 + L T V J + 1 Q I + 1 + L T
464 346 463 pm2.61dan φ V J < Q I + 1 + L T V J + 1 Q I + 1 + L T
465 323 464 mpdan φ V J + 1 Q I + 1 + L T
466 465 adantr φ x V J V J + 1 V J + 1 Q I + 1 + L T
467 182 adantr φ x V J V J + 1 V J + 1 Q I + 1 + L T x
468 197 ad2antrr φ x V J V J + 1 V J + 1 Q I + 1 + L T V J + 1
469 178 ad2antrr φ x V J V J + 1 V J + 1 Q I + 1 + L T Q I + 1 + L T
470 iooltub V J * V J + 1 * x V J V J + 1 x < V J + 1
471 193 199 200 470 syl3anc φ x V J V J + 1 x < V J + 1
472 471 adantr φ x V J V J + 1 V J + 1 Q I + 1 + L T x < V J + 1
473 simpr φ x V J V J + 1 V J + 1 Q I + 1 + L T V J + 1 Q I + 1 + L T
474 467 468 469 472 473 ltletrd φ x V J V J + 1 V J + 1 Q I + 1 + L T x < Q I + 1 + L T
475 466 474 mpdan φ x V J V J + 1 x < Q I + 1 + L T
476 174 180 182 203 475 eliood φ x V J V J + 1 x Q I + L T Q I + 1 + L T
477 476 ralrimiva φ x V J V J + 1 x Q I + L T Q I + 1 + L T
478 dfss3 V J V J + 1 Q I + L T Q I + 1 + L T x V J V J + 1 x Q I + L T Q I + 1 + L T
479 477 478 sylibr φ V J V J + 1 Q I + L T Q I + 1 + L T
480 fveq2 i = I Q i = Q I
481 480 oveq1d i = I Q i + l T = Q I + l T
482 oveq1 i = I i + 1 = I + 1
483 482 fveq2d i = I Q i + 1 = Q I + 1
484 483 oveq1d i = I Q i + 1 + l T = Q I + 1 + l T
485 481 484 oveq12d i = I Q i + l T Q i + 1 + l T = Q I + l T Q I + 1 + l T
486 485 sseq2d i = I V J V J + 1 Q i + l T Q i + 1 + l T V J V J + 1 Q I + l T Q I + 1 + l T
487 oveq1 l = L l T = L T
488 487 oveq2d l = L Q I + l T = Q I + L T
489 487 oveq2d l = L Q I + 1 + l T = Q I + 1 + L T
490 488 489 oveq12d l = L Q I + l T Q I + 1 + l T = Q I + L T Q I + 1 + L T
491 490 sseq2d l = L V J V J + 1 Q I + l T Q I + 1 + l T V J V J + 1 Q I + L T Q I + 1 + L T
492 486 491 rspc2ev I 0 ..^ M L V J V J + 1 Q I + L T Q I + 1 + L T i 0 ..^ M l V J V J + 1 Q i + l T Q i + 1 + l T
493 165 167 479 492 syl3anc φ i 0 ..^ M l V J V J + 1 Q i + l T Q i + 1 + l T
494 165 167 493 jca31 φ I 0 ..^ M L i 0 ..^ M l V J V J + 1 Q i + l T Q i + 1 + l T