Metamath Proof Explorer


Theorem ftc1anclem8

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 29-May-2018)

Ref Expression
Hypotheses ftc1anc.g G=xABAxFtdt
ftc1anc.a φA
ftc1anc.b φB
ftc1anc.le φAB
ftc1anc.s φABD
ftc1anc.d φD
ftc1anc.i φF𝐿1
ftc1anc.f φF:D
Assertion ftc1anclem8 φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwFtft+igt+ft+igt0<y

Proof

Step Hyp Ref Expression
1 ftc1anc.g G=xABAxFtdt
2 ftc1anc.a φA
3 ftc1anc.b φB
4 ftc1anc.le φAB
5 ftc1anc.s φABD
6 ftc1anc.d φD
7 ftc1anc.i φF𝐿1
8 ftc1anc.f φF:D
9 1 2 3 4 5 6 7 8 ftc1anclem7 φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0+2tiftuwFtft+igt0<y2+y2
10 simplll φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+φfdom1gdom1
11 3simpa uABwABuwuABwAB
12 ioossre uw
13 12 a1i φfdom1gdom1uw
14 rembl domvol
15 14 a1i φfdom1gdom1domvol
16 fvex ft+igtV
17 c0ex 0V
18 16 17 ifex iftuwft+igt0V
19 18 a1i φfdom1gdom1tuwiftuwft+igt0V
20 eldifn tuw¬tuw
21 20 adantl φfdom1gdom1tuw¬tuw
22 21 iffalsed φfdom1gdom1tuwiftuwft+igt0=0
23 iftrue tuwiftuwft+igt0=ft+igt
24 23 mpteq2ia tuwiftuwft+igt0=tuwft+igt
25 resmpt uwtft+igtuw=tuwft+igt
26 12 25 ax-mp tft+igtuw=tuwft+igt
27 24 26 eqtr4i tuwiftuwft+igt0=tft+igtuw
28 i1ff fdom1f:
29 28 ffvelrnda fdom1tft
30 29 recnd fdom1tft
31 ax-icn i
32 i1ff gdom1g:
33 32 ffvelrnda gdom1tgt
34 33 recnd gdom1tgt
35 mulcl igtigt
36 31 34 35 sylancr gdom1tigt
37 addcl ftigtft+igt
38 30 36 37 syl2an fdom1tgdom1tft+igt
39 38 anandirs fdom1gdom1tft+igt
40 reex V
41 40 a1i fdom1gdom1V
42 29 adantlr fdom1gdom1tft
43 36 adantll fdom1gdom1tigt
44 28 feqmptd fdom1f=tft
45 44 adantr fdom1gdom1f=tft
46 40 a1i gdom1V
47 31 a1i gdom1ti
48 fconstmpt ×i=ti
49 48 a1i gdom1×i=ti
50 32 feqmptd gdom1g=tgt
51 46 47 33 49 50 offval2 gdom1×i×fg=tigt
52 51 adantl fdom1gdom1×i×fg=tigt
53 41 42 43 45 52 offval2 fdom1gdom1f+f×i×fg=tft+igt
54 absf abs:
55 54 a1i fdom1gdom1abs:
56 55 feqmptd fdom1gdom1abs=xx
57 fveq2 x=ft+igtx=ft+igt
58 39 53 56 57 fmptco fdom1gdom1absf+f×i×fg=tft+igt
59 ftc1anclem3 fdom1gdom1absf+f×i×fgdom1
60 58 59 eqeltrrd fdom1gdom1tft+igtdom1
61 i1fmbf tft+igtdom1tft+igtMblFn
62 60 61 syl fdom1gdom1tft+igtMblFn
63 ioombl uwdomvol
64 mbfres tft+igtMblFnuwdomvoltft+igtuwMblFn
65 62 63 64 sylancl fdom1gdom1tft+igtuwMblFn
66 27 65 eqeltrid fdom1gdom1tuwiftuwft+igt0MblFn
67 66 adantl φfdom1gdom1tuwiftuwft+igt0MblFn
68 13 15 19 22 67 mbfss φfdom1gdom1tiftuwft+igt0MblFn
69 68 adantr φfdom1gdom1uABwABtiftuwft+igt0MblFn
70 39 abscld fdom1gdom1tft+igt
71 39 absge0d fdom1gdom1t0ft+igt
72 elrege0 ft+igt0+∞ft+igt0ft+igt
73 70 71 72 sylanbrc fdom1gdom1tft+igt0+∞
74 0e0icopnf 00+∞
75 ifcl ft+igt0+∞00+∞iftuwft+igt00+∞
76 73 74 75 sylancl fdom1gdom1tiftuwft+igt00+∞
77 76 fmpttd fdom1gdom1tiftuwft+igt0:0+∞
78 77 ad2antlr φfdom1gdom1uABwABtiftuwft+igt0:0+∞
79 70 rexrd fdom1gdom1tft+igt*
80 elxrge0 ft+igt0+∞ft+igt*0ft+igt
81 79 71 80 sylanbrc fdom1gdom1tft+igt0+∞
82 0e0iccpnf 00+∞
83 ifcl ft+igt0+∞00+∞iftuwft+igt00+∞
84 81 82 83 sylancl fdom1gdom1tiftuwft+igt00+∞
85 84 fmpttd fdom1gdom1tiftuwft+igt0:0+∞
86 85 ad2antlr φfdom1gdom1uABwABtiftuwft+igt0:0+∞
87 ifcl ft+igt0+∞00+∞iftDft+igt00+∞
88 81 82 87 sylancl fdom1gdom1tiftDft+igt00+∞
89 88 fmpttd fdom1gdom1tiftDft+igt0:0+∞
90 ffn f:fFn
91 frn f:ranf
92 ax-resscn
93 91 92 sstrdi f:ranf
94 ffn abs:absFn
95 54 94 ax-mp absFn
96 fnco absFnfFnranfabsfFn
97 95 96 mp3an1 fFnranfabsfFn
98 90 93 97 syl2anc f:absfFn
99 28 98 syl fdom1absfFn
100 99 adantr fdom1gdom1absfFn
101 ffn g:gFn
102 frn g:rang
103 102 92 sstrdi g:rang
104 fnco absFngFnrangabsgFn
105 95 104 mp3an1 gFnrangabsgFn
106 101 103 105 syl2anc g:absgFn
107 32 106 syl gdom1absgFn
108 107 adantl fdom1gdom1absgFn
109 inidm =
110 28 adantr fdom1gdom1f:
111 fvco3 f:tabsft=ft
112 110 111 sylan fdom1gdom1tabsft=ft
113 32 adantl fdom1gdom1g:
114 fvco3 g:tabsgt=gt
115 113 114 sylan fdom1gdom1tabsgt=gt
116 100 108 41 41 109 112 115 offval fdom1gdom1absf+fabsg=tft+gt
117 30 addid1d fdom1tft+0=ft
118 117 mpteq2dva fdom1tft+0=tft
119 40 a1i fdom1V
120 17 a1i fdom1t0V
121 31 a1i fdom1ti
122 48 a1i fdom1×i=ti
123 fconstmpt ×0=t0
124 123 a1i fdom1×0=t0
125 119 121 120 122 124 offval2 fdom1×i×f×0=ti0
126 it0e0 i0=0
127 126 mpteq2i ti0=t0
128 125 127 eqtrdi fdom1×i×f×0=t0
129 119 29 120 44 128 offval2 fdom1f+f×i×f×0=tft+0
130 118 129 44 3eqtr4d fdom1f+f×i×f×0=f
131 130 coeq2d fdom1absf+f×i×f×0=absf
132 i1f0 ×0dom1
133 ftc1anclem3 fdom1×0dom1absf+f×i×f×0dom1
134 132 133 mpan2 fdom1absf+f×i×f×0dom1
135 131 134 eqeltrrd fdom1absfdom1
136 135 adantr fdom1gdom1absfdom1
137 coeq2 f=gabsf=absg
138 137 eleq1d f=gabsfdom1absgdom1
139 138 135 vtoclga gdom1absgdom1
140 139 adantl fdom1gdom1absgdom1
141 136 140 i1fadd fdom1gdom1absf+fabsgdom1
142 116 141 eqeltrrd fdom1gdom1tft+gtdom1
143 30 abscld fdom1tft
144 30 absge0d fdom1t0ft
145 elrege0 ft0+∞ft0ft
146 143 144 145 sylanbrc fdom1tft0+∞
147 34 abscld gdom1tgt
148 34 absge0d gdom1t0gt
149 elrege0 gt0+∞gt0gt
150 147 148 149 sylanbrc gdom1tgt0+∞
151 ge0addcl ft0+∞gt0+∞ft+gt0+∞
152 146 150 151 syl2an fdom1tgdom1tft+gt0+∞
153 152 anandirs fdom1gdom1tft+gt0+∞
154 153 fmpttd fdom1gdom1tft+gt:0+∞
155 0plef tft+gt:0+∞tft+gt:0𝑝ftft+gt
156 154 155 sylib fdom1gdom1tft+gt:0𝑝ftft+gt
157 156 simprd fdom1gdom10𝑝ftft+gt
158 itg2itg1 tft+gtdom10𝑝ftft+gt2tft+gt=1tft+gt
159 itg1cl tft+gtdom11tft+gt
160 159 adantr tft+gtdom10𝑝ftft+gt1tft+gt
161 158 160 eqeltrd tft+gtdom10𝑝ftft+gt2tft+gt
162 142 157 161 syl2anc fdom1gdom12tft+gt
163 icossicc 0+∞0+∞
164 fss tft+gt:0+∞0+∞0+∞tft+gt:0+∞
165 154 163 164 sylancl fdom1gdom1tft+gt:0+∞
166 0re 0
167 ifcl ft+igt0iftDft+igt0
168 70 166 167 sylancl fdom1gdom1tiftDft+igt0
169 readdcl ftgtft+gt
170 143 147 169 syl2an fdom1tgdom1tft+gt
171 170 anandirs fdom1gdom1tft+gt
172 70 leidd fdom1gdom1tft+igtft+igt
173 breq1 ft+igt=iftDft+igt0ft+igtft+igtiftDft+igt0ft+igt
174 breq1 0=iftDft+igt00ft+igtiftDft+igt0ft+igt
175 173 174 ifboth ft+igtft+igt0ft+igtiftDft+igt0ft+igt
176 172 71 175 syl2anc fdom1gdom1tiftDft+igt0ft+igt
177 abstri ftigtft+igtft+igt
178 30 36 177 syl2an fdom1tgdom1tft+igtft+igt
179 178 anandirs fdom1gdom1tft+igtft+igt
180 absmul igtigt=igt
181 31 34 180 sylancr gdom1tigt=igt
182 absi i=1
183 182 oveq1i igt=1gt
184 181 183 eqtrdi gdom1tigt=1gt
185 147 recnd gdom1tgt
186 185 mulid2d gdom1t1gt=gt
187 184 186 eqtrd gdom1tigt=gt
188 187 adantll fdom1gdom1tigt=gt
189 188 oveq2d fdom1gdom1tft+igt=ft+gt
190 179 189 breqtrd fdom1gdom1tft+igtft+gt
191 168 70 171 176 190 letrd fdom1gdom1tiftDft+igt0ft+gt
192 191 ralrimiva fdom1gdom1tiftDft+igt0ft+gt
193 eqidd fdom1gdom1tiftDft+igt0=tiftDft+igt0
194 eqidd fdom1gdom1tft+gt=tft+gt
195 41 168 171 193 194 ofrfval2 fdom1gdom1tiftDft+igt0ftft+gttiftDft+igt0ft+gt
196 192 195 mpbird fdom1gdom1tiftDft+igt0ftft+gt
197 itg2le tiftDft+igt0:0+∞tft+gt:0+∞tiftDft+igt0ftft+gt2tiftDft+igt02tft+gt
198 89 165 196 197 syl3anc fdom1gdom12tiftDft+igt02tft+gt
199 itg2lecl tiftDft+igt0:0+∞2tft+gt2tiftDft+igt02tft+gt2tiftDft+igt0
200 89 162 198 199 syl3anc fdom1gdom12tiftDft+igt0
201 200 ad2antlr φfdom1gdom1uABwAB2tiftDft+igt0
202 89 ad2antlr φfdom1gdom1uABwABtiftDft+igt0:0+∞
203 breq1 ft+igt=iftuwft+igt0ft+igtiftDft+igt0iftuwft+igt0iftDft+igt0
204 breq1 0=iftuwft+igt00iftDft+igt0iftuwft+igt0iftDft+igt0
205 elioore tuwt
206 205 172 sylan2 fdom1gdom1tuwft+igtft+igt
207 206 adantll φfdom1gdom1tuwft+igtft+igt
208 207 adantlr φfdom1gdom1uABwABtuwft+igtft+igt
209 2 rexrd φA*
210 3 rexrd φB*
211 209 210 jca φA*B*
212 df-icc .=x*,y*t*|xtty
213 212 elixx3g uABA*B*u*AuuB
214 213 simprbi uABAuuB
215 214 simpld uABAu
216 212 elixx3g wABA*B*w*AwwB
217 216 simprbi wABAwwB
218 217 simprd wABwB
219 215 218 anim12i uABwABAuwB
220 ioossioo A*B*AuwBuwAB
221 211 219 220 syl2an φuABwABuwAB
222 5 adantr φuABwABABD
223 221 222 sstrd φuABwABuwD
224 223 sselda φuABwABtuwtD
225 iftrue tDiftDft+igt0=ft+igt
226 224 225 syl φuABwABtuwiftDft+igt0=ft+igt
227 226 adantllr φfdom1gdom1uABwABtuwiftDft+igt0=ft+igt
228 208 227 breqtrrd φfdom1gdom1uABwABtuwft+igtiftDft+igt0
229 breq2 ft+igt=iftDft+igt00ft+igt0iftDft+igt0
230 breq2 0=iftDft+igt0000iftDft+igt0
231 6 sselda φtDt
232 231 adantlr φfdom1gdom1tDt
233 71 adantll φfdom1gdom1t0ft+igt
234 232 233 syldan φfdom1gdom1tD0ft+igt
235 0le0 00
236 235 a1i φfdom1gdom1¬tD00
237 229 230 234 236 ifbothda φfdom1gdom10iftDft+igt0
238 237 ad2antrr φfdom1gdom1uABwAB¬tuw0iftDft+igt0
239 203 204 228 238 ifbothda φfdom1gdom1uABwABiftuwft+igt0iftDft+igt0
240 239 ralrimivw φfdom1gdom1uABwABtiftuwft+igt0iftDft+igt0
241 40 a1i φV
242 18 a1i φtiftuwft+igt0V
243 16 17 ifex iftDft+igt0V
244 243 a1i φtiftDft+igt0V
245 eqidd φtiftuwft+igt0=tiftuwft+igt0
246 eqidd φtiftDft+igt0=tiftDft+igt0
247 241 242 244 245 246 ofrfval2 φtiftuwft+igt0ftiftDft+igt0tiftuwft+igt0iftDft+igt0
248 247 ad2antrr φfdom1gdom1uABwABtiftuwft+igt0ftiftDft+igt0tiftuwft+igt0iftDft+igt0
249 240 248 mpbird φfdom1gdom1uABwABtiftuwft+igt0ftiftDft+igt0
250 itg2le tiftuwft+igt0:0+∞tiftDft+igt0:0+∞tiftuwft+igt0ftiftDft+igt02tiftuwft+igt02tiftDft+igt0
251 86 202 249 250 syl3anc φfdom1gdom1uABwAB2tiftuwft+igt02tiftDft+igt0
252 itg2lecl tiftuwft+igt0:0+∞2tiftDft+igt02tiftuwft+igt02tiftDft+igt02tiftuwft+igt0
253 86 201 251 252 syl3anc φfdom1gdom1uABwAB2tiftuwft+igt0
254 8 ffvelrnda φtDFt
255 254 adantlr φuABwABtDFt
256 224 255 syldan φuABwABtuwFt
257 256 adantllr φfdom1gdom1uABwABtuwFt
258 205 39 sylan2 fdom1gdom1tuwft+igt
259 258 adantll φfdom1gdom1tuwft+igt
260 259 adantlr φfdom1gdom1uABwABtuwft+igt
261 257 260 subcld φfdom1gdom1uABwABtuwFtft+igt
262 261 abscld φfdom1gdom1uABwABtuwFtft+igt
263 261 absge0d φfdom1gdom1uABwABtuw0Ftft+igt
264 elrege0 Ftft+igt0+∞Ftft+igt0Ftft+igt
265 262 263 264 sylanbrc φfdom1gdom1uABwABtuwFtft+igt0+∞
266 74 a1i φfdom1gdom1uABwAB¬tuw00+∞
267 265 266 ifclda φfdom1gdom1uABwABiftuwFtft+igt00+∞
268 267 adantr φfdom1gdom1uABwABtiftuwFtft+igt00+∞
269 268 fmpttd φfdom1gdom1uABwABtiftuwFtft+igt0:0+∞
270 262 rexrd φfdom1gdom1uABwABtuwFtft+igt*
271 elxrge0 Ftft+igt0+∞Ftft+igt*0Ftft+igt
272 270 263 271 sylanbrc φfdom1gdom1uABwABtuwFtft+igt0+∞
273 82 a1i φfdom1gdom1uABwAB¬tuw00+∞
274 272 273 ifclda φfdom1gdom1uABwABiftuwFtft+igt00+∞
275 274 adantr φfdom1gdom1uABwABtiftuwFtft+igt00+∞
276 275 fmpttd φfdom1gdom1uABwABtiftuwFtft+igt0:0+∞
277 recncf :cn
278 prid1g :cn
279 277 278 ax-mp
280 ftc1anclem2 F:DF𝐿12tiftDFt0
281 279 280 mp3an3 F:DF𝐿12tiftDFt0
282 8 7 281 syl2anc φ2tiftDFt0
283 imcncf :cn
284 prid2g :cn
285 283 284 ax-mp
286 ftc1anclem2 F:DF𝐿12tiftDFt0
287 285 286 mp3an3 F:DF𝐿12tiftDFt0
288 8 7 287 syl2anc φ2tiftDFt0
289 282 288 readdcld φ2tiftDFt0+2tiftDFt0
290 289 ad2antrr φfdom1gdom1uABwAB2tiftDFt0+2tiftDFt0
291 201 290 readdcld φfdom1gdom1uABwAB2tiftDft+igt0+2tiftDFt0+2tiftDFt0
292 ge0addcl x0+∞y0+∞x+y0+∞
293 292 adantl φfdom1gdom1x0+∞y0+∞x+y0+∞
294 ifcl ft+igt0+∞00+∞iftDft+igt00+∞
295 73 74 294 sylancl fdom1gdom1tiftDft+igt00+∞
296 295 fmpttd fdom1gdom1tiftDft+igt0:0+∞
297 296 adantl φfdom1gdom1tiftDft+igt0:0+∞
298 292 adantl φx0+∞y0+∞x+y0+∞
299 254 recld φtDFt
300 299 recnd φtDFt
301 300 abscld φtDFt
302 300 absge0d φtD0Ft
303 elrege0 Ft0+∞Ft0Ft
304 301 302 303 sylanbrc φtDFt0+∞
305 74 a1i φ¬tD00+∞
306 304 305 ifclda φiftDFt00+∞
307 306 adantr φtiftDFt00+∞
308 307 fmpttd φtiftDFt0:0+∞
309 254 imcld φtDFt
310 309 recnd φtDFt
311 310 abscld φtDFt
312 310 absge0d φtD0Ft
313 elrege0 Ft0+∞Ft0Ft
314 311 312 313 sylanbrc φtDFt0+∞
315 314 305 ifclda φiftDFt00+∞
316 315 adantr φtiftDFt00+∞
317 316 fmpttd φtiftDFt0:0+∞
318 298 308 317 241 241 109 off φtiftDFt0+ftiftDFt0:0+∞
319 318 adantr φfdom1gdom1tiftDFt0+ftiftDFt0:0+∞
320 40 a1i φfdom1gdom1V
321 293 297 319 320 320 109 off φfdom1gdom1tiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞
322 fss tiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞0+∞0+∞tiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞
323 321 163 322 sylancl φfdom1gdom1tiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞
324 323 adantr φfdom1gdom1uABwABtiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞
325 0xr 0*
326 325 a1i φfdom1gdom1uABwAB¬tuw0*
327 270 326 ifclda φfdom1gdom1uABwABiftuwFtft+igt0*
328 254 adantlr φfdom1gdom1tDFt
329 39 adantll φfdom1gdom1tft+igt
330 232 329 syldan φfdom1gdom1tDft+igt
331 328 330 subcld φfdom1gdom1tDFtft+igt
332 331 abscld φfdom1gdom1tDFtft+igt
333 332 rexrd φfdom1gdom1tDFtft+igt*
334 325 a1i φfdom1gdom1¬tD0*
335 333 334 ifclda φfdom1gdom1iftDFtft+igt0*
336 335 adantr φfdom1gdom1uABwABiftDFtft+igt0*
337 330 abscld φfdom1gdom1tDft+igt
338 0red φfdom1gdom1¬tD0
339 337 338 ifclda φfdom1gdom1iftDft+igt0
340 0red φ¬tD0
341 301 340 ifclda φiftDFt0
342 311 340 ifclda φiftDFt0
343 341 342 readdcld φiftDFt0+iftDFt0
344 343 adantr φfdom1gdom1iftDFt0+iftDFt0
345 339 344 readdcld φfdom1gdom1iftDft+igt0+iftDFt0+iftDFt0
346 345 rexrd φfdom1gdom1iftDft+igt0+iftDFt0+iftDFt0*
347 346 adantr φfdom1gdom1uABwABiftDft+igt0+iftDFt0+iftDFt0*
348 breq1 Ftft+igt=iftuwFtft+igt0Ftft+igtiftDFtft+igt0iftuwFtft+igt0iftDFtft+igt0
349 breq1 0=iftuwFtft+igt00iftDFtft+igt0iftuwFtft+igt0iftDFtft+igt0
350 224 adantllr φfdom1gdom1uABwABtuwtD
351 332 leidd φfdom1gdom1tDFtft+igtFtft+igt
352 351 adantlr φfdom1gdom1uABwABtDFtft+igtFtft+igt
353 iftrue tDiftDFtft+igt0=Ftft+igt
354 353 adantl φfdom1gdom1uABwABtDiftDFtft+igt0=Ftft+igt
355 352 354 breqtrrd φfdom1gdom1uABwABtDFtft+igtiftDFtft+igt0
356 350 355 syldan φfdom1gdom1uABwABtuwFtft+igtiftDFtft+igt0
357 breq2 Ftft+igt=iftDFtft+igt00Ftft+igt0iftDFtft+igt0
358 breq2 0=iftDFtft+igt0000iftDFtft+igt0
359 331 absge0d φfdom1gdom1tD0Ftft+igt
360 357 358 359 236 ifbothda φfdom1gdom10iftDFtft+igt0
361 360 ad2antrr φfdom1gdom1uABwAB¬tuw0iftDFtft+igt0
362 348 349 356 361 ifbothda φfdom1gdom1uABwABiftuwFtft+igt0iftDFtft+igt0
363 254 negcld φtDFt
364 363 adantlr φfdom1gdom1tDFt
365 330 364 addcld φfdom1gdom1tDft+igt+Ft
366 365 abscld φfdom1gdom1tDft+igt+Ft
367 363 abscld φtDFt
368 367 adantlr φfdom1gdom1tDFt
369 337 368 readdcld φfdom1gdom1tDft+igt+Ft
370 301 311 readdcld φtDFt+Ft
371 370 adantlr φfdom1gdom1tDFt+Ft
372 337 371 readdcld φfdom1gdom1tDft+igt+Ft+Ft
373 330 364 abstrid φfdom1gdom1tDft+igt+Ftft+igt+Ft
374 mulcl iFtiFt
375 31 310 374 sylancr φtDiFt
376 300 375 abstrid φtDFt+iFtFt+iFt
377 254 absnegd φtDFt=Ft
378 254 replimd φtDFt=Ft+iFt
379 378 fveq2d φtDFt=Ft+iFt
380 377 379 eqtrd φtDFt=Ft+iFt
381 absmul iFtiFt=iFt
382 31 310 381 sylancr φtDiFt=iFt
383 182 oveq1i iFt=1Ft
384 382 383 eqtrdi φtDiFt=1Ft
385 311 recnd φtDFt
386 385 mulid2d φtD1Ft=Ft
387 384 386 eqtr2d φtDFt=iFt
388 387 oveq2d φtDFt+Ft=Ft+iFt
389 376 380 388 3brtr4d φtDFtFt+Ft
390 389 adantlr φfdom1gdom1tDFtFt+Ft
391 368 371 337 390 leadd2dd φfdom1gdom1tDft+igt+Ftft+igt+Ft+Ft
392 366 369 372 373 391 letrd φfdom1gdom1tDft+igt+Ftft+igt+Ft+Ft
393 328 330 abssubd φfdom1gdom1tDFtft+igt=ft+igt-Ft
394 353 adantl φfdom1gdom1tDiftDFtft+igt0=Ftft+igt
395 330 328 negsubd φfdom1gdom1tDft+igt+Ft=ft+igt-Ft
396 395 fveq2d φfdom1gdom1tDft+igt+Ft=ft+igt-Ft
397 393 394 396 3eqtr4d φfdom1gdom1tDiftDFtft+igt0=ft+igt+Ft
398 iftrue tDiftDft+igt+Ft+Ft0=ft+igt+Ft+Ft
399 398 adantl φfdom1gdom1tDiftDft+igt+Ft+Ft0=ft+igt+Ft+Ft
400 392 397 399 3brtr4d φfdom1gdom1tDiftDFtft+igt0iftDft+igt+Ft+Ft0
401 400 ex φfdom1gdom1tDiftDFtft+igt0iftDft+igt+Ft+Ft0
402 235 a1i ¬tD00
403 iffalse ¬tDiftDFtft+igt0=0
404 iffalse ¬tDiftDft+igt+Ft+Ft0=0
405 402 403 404 3brtr4d ¬tDiftDFtft+igt0iftDft+igt+Ft+Ft0
406 401 405 pm2.61d1 φfdom1gdom1iftDFtft+igt0iftDft+igt+Ft+Ft0
407 iftrue tDiftDFt0=Ft
408 iftrue tDiftDFt0=Ft
409 407 408 oveq12d tDiftDFt0+iftDFt0=Ft+Ft
410 225 409 oveq12d tDiftDft+igt0+iftDFt0+iftDFt0=ft+igt+Ft+Ft
411 410 398 eqtr4d tDiftDft+igt0+iftDFt0+iftDFt0=iftDft+igt+Ft+Ft0
412 00id 0+0=0
413 412 oveq2i 0+0+0=0+0
414 413 412 eqtri 0+0+0=0
415 iffalse ¬tDiftDft+igt0=0
416 iffalse ¬tDiftDFt0=0
417 iffalse ¬tDiftDFt0=0
418 416 417 oveq12d ¬tDiftDFt0+iftDFt0=0+0
419 415 418 oveq12d ¬tDiftDft+igt0+iftDFt0+iftDFt0=0+0+0
420 414 419 404 3eqtr4a ¬tDiftDft+igt0+iftDFt0+iftDFt0=iftDft+igt+Ft+Ft0
421 411 420 pm2.61i iftDft+igt0+iftDFt0+iftDFt0=iftDft+igt+Ft+Ft0
422 406 421 breqtrrdi φfdom1gdom1iftDFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
423 422 adantr φfdom1gdom1uABwABiftDFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
424 327 336 347 362 423 xrletrd φfdom1gdom1uABwABiftuwFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
425 424 ralrimivw φfdom1gdom1uABwABtiftuwFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
426 fvex Ftft+igtV
427 426 17 ifex iftuwFtft+igt0V
428 427 a1i φtiftuwFtft+igt0V
429 ovexd φtiftDft+igt0+iftDFt0+iftDFt0V
430 eqidd φtiftuwFtft+igt0=tiftuwFtft+igt0
431 ovexd φtiftDFt0+iftDFt0V
432 341 adantr φtiftDFt0
433 342 adantr φtiftDFt0
434 eqidd φtiftDFt0=tiftDFt0
435 eqidd φtiftDFt0=tiftDFt0
436 241 432 433 434 435 offval2 φtiftDFt0+ftiftDFt0=tiftDFt0+iftDFt0
437 241 244 431 246 436 offval2 φtiftDft+igt0+ftiftDFt0+ftiftDFt0=tiftDft+igt0+iftDFt0+iftDFt0
438 241 428 429 430 437 ofrfval2 φtiftuwFtft+igt0ftiftDft+igt0+ftiftDFt0+ftiftDFt0tiftuwFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
439 438 ad2antrr φfdom1gdom1uABwABtiftuwFtft+igt0ftiftDft+igt0+ftiftDFt0+ftiftDFt0tiftuwFtft+igt0iftDft+igt0+iftDFt0+iftDFt0
440 425 439 mpbird φfdom1gdom1uABwABtiftuwFtft+igt0ftiftDft+igt0+ftiftDFt0+ftiftDFt0
441 itg2le tiftuwFtft+igt0:0+∞tiftDft+igt0+ftiftDFt0+ftiftDFt0:0+∞tiftuwFtft+igt0ftiftDft+igt0+ftiftDFt0+ftiftDFt02tiftuwFtft+igt02tiftDft+igt0+ftiftDFt0+ftiftDFt0
442 276 324 440 441 syl3anc φfdom1gdom1uABwAB2tiftuwFtft+igt02tiftDft+igt0+ftiftDFt0+ftiftDFt0
443 6 adantr φfdom1gdom1D
444 243 a1i φfdom1gdom1tDiftDft+igt0V
445 eldifn tD¬tD
446 445 iffalsed tDiftDft+igt0=0
447 446 adantl φfdom1gdom1tDiftDft+igt0=0
448 ovexd fdom1gdom1tigtV
449 41 42 448 45 52 offval2 fdom1gdom1f+f×i×fg=tft+igt
450 39 449 56 57 fmptco fdom1gdom1absf+f×i×fg=tft+igt
451 450 reseq1d fdom1gdom1absf+f×i×fgD=tft+igtD
452 6 resmptd φtft+igtD=tDft+igt
453 451 452 sylan9eqr φfdom1gdom1absf+f×i×fgD=tDft+igt
454 225 mpteq2ia tDiftDft+igt0=tDft+igt
455 453 454 eqtr4di φfdom1gdom1absf+f×i×fgD=tDiftDft+igt0
456 i1fmbf absf+f×i×fgdom1absf+f×i×fgMblFn
457 59 456 syl fdom1gdom1absf+f×i×fgMblFn
458 8 fdmd φdomF=D
459 iblmbf F𝐿1FMblFn
460 mbfdm FMblFndomFdomvol
461 7 459 460 3syl φdomFdomvol
462 458 461 eqeltrrd φDdomvol
463 mbfres absf+f×i×fgMblFnDdomvolabsf+f×i×fgDMblFn
464 457 462 463 syl2anr φfdom1gdom1absf+f×i×fgDMblFn
465 455 464 eqeltrrd φfdom1gdom1tDiftDft+igt0MblFn
466 443 15 444 447 465 mbfss φfdom1gdom1tiftDft+igt0MblFn
467 200 adantl φfdom1gdom12tiftDft+igt0
468 0cnd φ¬tD0
469 300 468 ifclda φiftDFt0
470 469 adantr φtiftDFt0
471 eqidd φtiftDFt0=tiftDFt0
472 54 a1i φabs:
473 472 feqmptd φabs=xx
474 fveq2 x=iftDFt0x=iftDFt0
475 fvif iftDFt0=iftDFt0
476 abs0 0=0
477 ifeq2 0=0iftDFt0=iftDFt0
478 476 477 ax-mp iftDFt0=iftDFt0
479 475 478 eqtri iftDFt0=iftDFt0
480 474 479 eqtrdi x=iftDFt0x=iftDFt0
481 470 471 473 480 fmptco φabstiftDFt0=tiftDFt0
482 299 340 ifclda φiftDFt0
483 482 adantr φtiftDFt0
484 483 fmpttd φtiftDFt0:
485 14 a1i φdomvol
486 482 adantr φtDiftDFt0
487 445 adantl φtD¬tD
488 487 iffalsed φtDiftDFt0=0
489 iftrue tDiftDFt0=Ft
490 489 mpteq2ia tDiftDFt0=tDFt
491 8 feqmptd φF=tDFt
492 7 459 syl φFMblFn
493 491 492 eqeltrrd φtDFtMblFn
494 254 ismbfcn2 φtDFtMblFntDFtMblFntDFtMblFn
495 493 494 mpbid φtDFtMblFntDFtMblFn
496 495 simpld φtDFtMblFn
497 490 496 eqeltrid φtDiftDFt0MblFn
498 6 485 486 488 497 mbfss φtiftDFt0MblFn
499 ftc1anclem1 tiftDFt0:tiftDFt0MblFnabstiftDFt0MblFn
500 484 498 499 syl2anc φabstiftDFt0MblFn
501 481 500 eqeltrrd φtiftDFt0MblFn
502 501 308 282 317 288 itg2addnc φ2tiftDFt0+ftiftDFt0=2tiftDFt0+2tiftDFt0
503 502 289 eqeltrd φ2tiftDFt0+ftiftDFt0
504 503 adantr φfdom1gdom12tiftDFt0+ftiftDFt0
505 466 297 467 319 504 itg2addnc φfdom1gdom12tiftDft+igt0+ftiftDFt0+ftiftDFt0=2tiftDft+igt0+2tiftDFt0+ftiftDFt0
506 502 adantr φfdom1gdom12tiftDFt0+ftiftDFt0=2tiftDFt0+2tiftDFt0
507 506 oveq2d φfdom1gdom12tiftDft+igt0+2tiftDFt0+ftiftDFt0=2tiftDft+igt0+2tiftDFt0+2tiftDFt0
508 505 507 eqtrd φfdom1gdom12tiftDft+igt0+ftiftDFt0+ftiftDFt0=2tiftDft+igt0+2tiftDFt0+2tiftDFt0
509 508 adantr φfdom1gdom1uABwAB2tiftDft+igt0+ftiftDFt0+ftiftDFt0=2tiftDft+igt0+2tiftDFt0+2tiftDFt0
510 442 509 breqtrd φfdom1gdom1uABwAB2tiftuwFtft+igt02tiftDft+igt0+2tiftDFt0+2tiftDFt0
511 itg2lecl tiftuwFtft+igt0:0+∞2tiftDft+igt0+2tiftDFt0+2tiftDFt02tiftuwFtft+igt02tiftDft+igt0+2tiftDFt0+2tiftDFt02tiftuwFtft+igt0
512 276 291 510 511 syl3anc φfdom1gdom1uABwAB2tiftuwFtft+igt0
513 69 78 253 269 512 itg2addnc φfdom1gdom1uABwAB2tiftuwft+igt0+ftiftuwFtft+igt0=2tiftuwft+igt0+2tiftuwFtft+igt0
514 241 242 428 245 430 offval2 φtiftuwft+igt0+ftiftuwFtft+igt0=tiftuwft+igt0+iftuwFtft+igt0
515 eqeq2 ft+igt+Ftft+igt=iftuwft+igt+Ftft+igt0iftuwft+igt0+iftuwFtft+igt0=ft+igt+Ftft+igtiftuwft+igt0+iftuwFtft+igt0=iftuwft+igt+Ftft+igt0
516 eqeq2 0=iftuwft+igt+Ftft+igt0iftuwft+igt0+iftuwFtft+igt0=0iftuwft+igt0+iftuwFtft+igt0=iftuwft+igt+Ftft+igt0
517 iftrue tuwiftuwFtft+igt0=Ftft+igt
518 23 517 oveq12d tuwiftuwft+igt0+iftuwFtft+igt0=ft+igt+Ftft+igt
519 518 adantl φtuwiftuwft+igt0+iftuwFtft+igt0=ft+igt+Ftft+igt
520 iffalse ¬tuwiftuwft+igt0=0
521 iffalse ¬tuwiftuwFtft+igt0=0
522 520 521 oveq12d ¬tuwiftuwft+igt0+iftuwFtft+igt0=0+0
523 522 412 eqtrdi ¬tuwiftuwft+igt0+iftuwFtft+igt0=0
524 523 adantl φ¬tuwiftuwft+igt0+iftuwFtft+igt0=0
525 515 516 519 524 ifbothda φiftuwft+igt0+iftuwFtft+igt0=iftuwft+igt+Ftft+igt0
526 525 mpteq2dv φtiftuwft+igt0+iftuwFtft+igt0=tiftuwft+igt+Ftft+igt0
527 514 526 eqtrd φtiftuwft+igt0+ftiftuwFtft+igt0=tiftuwft+igt+Ftft+igt0
528 527 ad2antrr φfdom1gdom1uABwABtiftuwft+igt0+ftiftuwFtft+igt0=tiftuwft+igt+Ftft+igt0
529 simplr φfdom1gdom1uABwABfdom1gdom1
530 258 abscld fdom1gdom1tuwft+igt
531 530 recnd fdom1gdom1tuwft+igt
532 529 531 sylan φfdom1gdom1uABwABtuwft+igt
533 262 recnd φfdom1gdom1uABwABtuwFtft+igt
534 532 533 addcomd φfdom1gdom1uABwABtuwft+igt+Ftft+igt=Ftft+igt+ft+igt
535 534 ifeq1da φfdom1gdom1uABwABiftuwft+igt+Ftft+igt0=iftuwFtft+igt+ft+igt0
536 535 mpteq2dv φfdom1gdom1uABwABtiftuwft+igt+Ftft+igt0=tiftuwFtft+igt+ft+igt0
537 528 536 eqtrd φfdom1gdom1uABwABtiftuwft+igt0+ftiftuwFtft+igt0=tiftuwFtft+igt+ft+igt0
538 537 fveq2d φfdom1gdom1uABwAB2tiftuwft+igt0+ftiftuwFtft+igt0=2tiftuwFtft+igt+ft+igt0
539 513 538 eqtr3d φfdom1gdom1uABwAB2tiftuwft+igt0+2tiftuwFtft+igt0=2tiftuwFtft+igt+ft+igt0
540 10 11 539 syl2an φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuw2tiftuwft+igt0+2tiftuwFtft+igt0=2tiftuwFtft+igt+ft+igt0
541 540 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0+2tiftuwFtft+igt0=2tiftuwFtft+igt+ft+igt0
542 rpcn y+y
543 542 2halvesd y+y2+y2=y
544 543 ad3antlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<y2+y2=y
545 9 541 544 3brtr3d φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwFtft+igt+ft+igt0<y