Metamath Proof Explorer


Theorem ftc1anclem7

Description: Lemma for ftc1anc . (Contributed by Brendan Leahy, 13-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 ftc1anclem7 φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0+2tiftuwFtft+igt0<y2+y2

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 i1ff fdom1f:
10 9 ffvelrnda fdom1xfx
11 10 recnd fdom1xfx
12 ax-icn i
13 i1ff gdom1g:
14 13 ffvelrnda gdom1xgx
15 14 recnd gdom1xgx
16 mulcl igxigx
17 12 15 16 sylancr gdom1xigx
18 addcl fxigxfx+igx
19 11 17 18 syl2an fdom1xgdom1xfx+igx
20 19 anandirs fdom1gdom1xfx+igx
21 reex V
22 21 a1i fdom1gdom1V
23 10 adantlr fdom1gdom1xfx
24 ovexd fdom1gdom1xigxV
25 9 feqmptd fdom1f=xfx
26 25 adantr fdom1gdom1f=xfx
27 21 a1i gdom1V
28 12 a1i gdom1xi
29 fconstmpt ×i=xi
30 29 a1i gdom1×i=xi
31 13 feqmptd gdom1g=xgx
32 27 28 14 30 31 offval2 gdom1×i×fg=xigx
33 32 adantl fdom1gdom1×i×fg=xigx
34 22 23 24 26 33 offval2 fdom1gdom1f+f×i×fg=xfx+igx
35 absf abs:
36 35 a1i fdom1gdom1abs:
37 36 feqmptd fdom1gdom1abs=tt
38 fveq2 t=fx+igxt=fx+igx
39 20 34 37 38 fmptco fdom1gdom1absf+f×i×fg=xfx+igx
40 ftc1anclem3 fdom1gdom1absf+f×i×fgdom1
41 39 40 eqeltrrd fdom1gdom1xfx+igxdom1
42 ioombl uwdomvol
43 fveq2 x=tfx=ft
44 fveq2 x=tgx=gt
45 44 oveq2d x=tigx=igt
46 43 45 oveq12d x=tfx+igx=ft+igt
47 46 fveq2d x=tfx+igx=ft+igt
48 eqid xfx+igx=xfx+igx
49 fvex ft+igtV
50 47 48 49 fvmpt txfx+igxt=ft+igt
51 50 eqcomd tft+igt=xfx+igxt
52 51 ifeq1d tiftuwft+igt0=iftuwxfx+igxt0
53 52 mpteq2ia tiftuwft+igt0=tiftuwxfx+igxt0
54 53 i1fres xfx+igxdom1uwdomvoltiftuwft+igt0dom1
55 41 42 54 sylancl fdom1gdom1tiftuwft+igt0dom1
56 breq2 ft+igt=iftuwft+igt00ft+igt0iftuwft+igt0
57 breq2 0=iftuwft+igt0000iftuwft+igt0
58 elioore tuwt
59 eleq1w x=txt
60 59 anbi2d x=tfdom1gdom1xfdom1gdom1t
61 46 eleq1d x=tfx+igxft+igt
62 60 61 imbi12d x=tfdom1gdom1xfx+igxfdom1gdom1tft+igt
63 62 20 chvarvv fdom1gdom1tft+igt
64 63 absge0d fdom1gdom1t0ft+igt
65 58 64 sylan2 fdom1gdom1tuw0ft+igt
66 0le0 00
67 66 a1i fdom1gdom1¬tuw00
68 56 57 65 67 ifbothda fdom1gdom10iftuwft+igt0
69 68 ralrimivw fdom1gdom1t0iftuwft+igt0
70 ax-resscn
71 70 a1i fdom1gdom1
72 c0ex 0V
73 49 72 ifex iftuwft+igt0V
74 eqid tiftuwft+igt0=tiftuwft+igt0
75 73 74 fnmpti tiftuwft+igt0Fn
76 75 a1i fdom1gdom1tiftuwft+igt0Fn
77 71 76 0pledm fdom1gdom10𝑝ftiftuwft+igt0×0ftiftuwft+igt0
78 72 a1i fdom1gdom1t0V
79 73 a1i fdom1gdom1tiftuwft+igt0V
80 fconstmpt ×0=t0
81 80 a1i fdom1gdom1×0=t0
82 eqidd fdom1gdom1tiftuwft+igt0=tiftuwft+igt0
83 22 78 79 81 82 ofrfval2 fdom1gdom1×0ftiftuwft+igt0t0iftuwft+igt0
84 77 83 bitrd fdom1gdom10𝑝ftiftuwft+igt0t0iftuwft+igt0
85 69 84 mpbird fdom1gdom10𝑝ftiftuwft+igt0
86 itg2itg1 tiftuwft+igt0dom10𝑝ftiftuwft+igt02tiftuwft+igt0=1tiftuwft+igt0
87 itg1cl tiftuwft+igt0dom11tiftuwft+igt0
88 87 adantr tiftuwft+igt0dom10𝑝ftiftuwft+igt01tiftuwft+igt0
89 86 88 eqeltrd tiftuwft+igt0dom10𝑝ftiftuwft+igt02tiftuwft+igt0
90 55 85 89 syl2anc fdom1gdom12tiftuwft+igt0
91 90 ad6antlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0
92 simplll φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+φfdom1gdom1
93 2 rexrd φA*
94 3 rexrd φB*
95 93 94 jca φA*B*
96 df-icc .=x*,y*t*|xtty
97 96 elixx3g uABA*B*u*AuuB
98 97 simprbi uABAuuB
99 98 simpld uABAu
100 96 elixx3g wABA*B*w*AwwB
101 100 simprbi wABAwwB
102 101 simprd wABwB
103 99 102 anim12i uABwABAuwB
104 ioossioo A*B*AuwBuwAB
105 95 103 104 syl2an φuABwABuwAB
106 5 adantr φuABwABABD
107 105 106 sstrd φuABwABuwD
108 107 3adantr3 φuABwABuwuwD
109 108 sselda φuABwABuwtuwtD
110 8 ffvelrnda φtDFt
111 110 adantlr φuABwABuwtDFt
112 109 111 syldan φuABwABuwtuwFt
113 112 adantllr φfdom1gdom1uABwABuwtuwFt
114 63 adantll φfdom1gdom1tft+igt
115 58 114 sylan2 φfdom1gdom1tuwft+igt
116 115 adantlr φfdom1gdom1uABwABuwtuwft+igt
117 113 116 subcld φfdom1gdom1uABwABuwtuwFtft+igt
118 117 abscld φfdom1gdom1uABwABuwtuwFtft+igt
119 118 rexrd φfdom1gdom1uABwABuwtuwFtft+igt*
120 117 absge0d φfdom1gdom1uABwABuwtuw0Ftft+igt
121 elxrge0 Ftft+igt0+∞Ftft+igt*0Ftft+igt
122 119 120 121 sylanbrc φfdom1gdom1uABwABuwtuwFtft+igt0+∞
123 0e0iccpnf 00+∞
124 123 a1i φfdom1gdom1uABwABuw¬tuw00+∞
125 122 124 ifclda φfdom1gdom1uABwABuwiftuwFtft+igt00+∞
126 125 adantr φfdom1gdom1uABwABuwtiftuwFtft+igt00+∞
127 126 fmpttd φfdom1gdom1uABwABuwtiftuwFtft+igt0:0+∞
128 92 127 sylan φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwtiftuwFtft+igt0:0+∞
129 rpre y+y
130 129 rehalfcld y+y2
131 130 ad2antlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwy2
132 simpll φfdom1gdom12tiftDFt0ft+igt<y2y+φfdom1gdom1
133 107 sselda φuABwABtuwtD
134 133 adantllr φfdom1gdom1uABwABtuwtD
135 110 adantlr φfdom1gdom1tDFt
136 6 sselda φtDt
137 136 adantlr φfdom1gdom1tDt
138 137 114 syldan φfdom1gdom1tDft+igt
139 135 138 subcld φfdom1gdom1tDFtft+igt
140 139 abscld φfdom1gdom1tDFtft+igt
141 140 rexrd φfdom1gdom1tDFtft+igt*
142 141 adantlr φfdom1gdom1uABwABtDFtft+igt*
143 134 142 syldan φfdom1gdom1uABwABtuwFtft+igt*
144 139 absge0d φfdom1gdom1tD0Ftft+igt
145 144 adantlr φfdom1gdom1uABwABtD0Ftft+igt
146 134 145 syldan φfdom1gdom1uABwABtuw0Ftft+igt
147 143 146 121 sylanbrc φfdom1gdom1uABwABtuwFtft+igt0+∞
148 123 a1i φfdom1gdom1uABwAB¬tuw00+∞
149 147 148 ifclda φfdom1gdom1uABwABiftuwFtft+igt00+∞
150 149 adantr φfdom1gdom1uABwABtiftuwFtft+igt00+∞
151 150 fmpttd φfdom1gdom1uABwABtiftuwFtft+igt0:0+∞
152 itg2cl tiftuwFtft+igt0:0+∞2tiftuwFtft+igt0*
153 151 152 syl φfdom1gdom1uABwAB2tiftuwFtft+igt0*
154 132 153 sylan φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftuwFtft+igt0*
155 rphalfcl y+y2+
156 155 rpxrd y+y2*
157 156 ad2antlr φfdom1gdom12tiftDFt0ft+igt<y2y+uABwABy2*
158 0cnd φ¬tD0
159 110 158 ifclda φiftDFt0
160 subcl iftDFt0ft+igtiftDFt0ft+igt
161 159 63 160 syl2an φfdom1gdom1tiftDFt0ft+igt
162 161 anassrs φfdom1gdom1tiftDFt0ft+igt
163 162 abscld φfdom1gdom1tiftDFt0ft+igt
164 163 rexrd φfdom1gdom1tiftDFt0ft+igt*
165 162 absge0d φfdom1gdom1t0iftDFt0ft+igt
166 elxrge0 iftDFt0ft+igt0+∞iftDFt0ft+igt*0iftDFt0ft+igt
167 164 165 166 sylanbrc φfdom1gdom1tiftDFt0ft+igt0+∞
168 167 fmpttd φfdom1gdom1tiftDFt0ft+igt:0+∞
169 itg2cl tiftDFt0ft+igt:0+∞2tiftDFt0ft+igt*
170 168 169 syl φfdom1gdom12tiftDFt0ft+igt*
171 170 ad3antrrr φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftDFt0ft+igt*
172 168 adantr φfdom1gdom1uABwABtiftDFt0ft+igt:0+∞
173 breq1 Ftft+igt=iftuwFtft+igt0Ftft+igtiftDFt0ft+igtiftuwFtft+igt0iftDFt0ft+igt
174 breq1 0=iftuwFtft+igt00iftDFt0ft+igtiftuwFtft+igt0iftDFt0ft+igt
175 140 leidd φfdom1gdom1tDFtft+igtFtft+igt
176 iftrue tDiftDFt0=Ft
177 176 fvoveq1d tDiftDFt0ft+igt=Ftft+igt
178 177 adantl φfdom1gdom1tDiftDFt0ft+igt=Ftft+igt
179 175 178 breqtrrd φfdom1gdom1tDFtft+igtiftDFt0ft+igt
180 179 adantlr φfdom1gdom1uABwABtDFtft+igtiftDFt0ft+igt
181 134 180 syldan φfdom1gdom1uABwABtuwFtft+igtiftDFt0ft+igt
182 181 adantlr φfdom1gdom1uABwABttuwFtft+igtiftDFt0ft+igt
183 165 adantlr φfdom1gdom1uABwABt0iftDFt0ft+igt
184 183 adantr φfdom1gdom1uABwABt¬tuw0iftDFt0ft+igt
185 173 174 182 184 ifbothda φfdom1gdom1uABwABtiftuwFtft+igt0iftDFt0ft+igt
186 185 ralrimiva φfdom1gdom1uABwABtiftuwFtft+igt0iftDFt0ft+igt
187 21 a1i φV
188 fvex Ftft+igtV
189 188 72 ifex iftuwFtft+igt0V
190 189 a1i φtiftuwFtft+igt0V
191 fvexd φtiftDFt0ft+igtV
192 eqidd φtiftuwFtft+igt0=tiftuwFtft+igt0
193 eqidd φtiftDFt0ft+igt=tiftDFt0ft+igt
194 187 190 191 192 193 ofrfval2 φtiftuwFtft+igt0ftiftDFt0ft+igttiftuwFtft+igt0iftDFt0ft+igt
195 194 ad2antrr φfdom1gdom1uABwABtiftuwFtft+igt0ftiftDFt0ft+igttiftuwFtft+igt0iftDFt0ft+igt
196 186 195 mpbird φfdom1gdom1uABwABtiftuwFtft+igt0ftiftDFt0ft+igt
197 itg2le tiftuwFtft+igt0:0+∞tiftDFt0ft+igt:0+∞tiftuwFtft+igt0ftiftDFt0ft+igt2tiftuwFtft+igt02tiftDFt0ft+igt
198 151 172 196 197 syl3anc φfdom1gdom1uABwAB2tiftuwFtft+igt02tiftDFt0ft+igt
199 132 198 sylan φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftuwFtft+igt02tiftDFt0ft+igt
200 simpllr φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftDFt0ft+igt<y2
201 154 171 157 199 200 xrlelttrd φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftuwFtft+igt0<y2
202 154 157 201 xrltled φfdom1gdom12tiftDFt0ft+igt<y2y+uABwAB2tiftuwFtft+igt0y2
203 202 adantllr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwAB2tiftuwFtft+igt0y2
204 203 3adantr3 φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuw2tiftuwFtft+igt0y2
205 itg2lecl tiftuwFtft+igt0:0+∞y22tiftuwFtft+igt0y22tiftuwFtft+igt0
206 128 131 204 205 syl3anc φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuw2tiftuwFtft+igt0
207 206 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwFtft+igt0
208 130 ad3antlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<y2
209 90 adantr fdom1gdom1rranfrangr02tiftuwft+igt0
210 2rp 2+
211 imassrn absranfrangranabs
212 frn abs:ranabs
213 35 212 ax-mp ranabs
214 211 213 sstri absranfrang
215 214 a1i fdom1gdom1absranfrang
216 9 frnd fdom1ranf
217 216 adantr fdom1gdom1ranf
218 13 frnd gdom1rang
219 218 adantl fdom1gdom1rang
220 217 219 unssd fdom1gdom1ranfrang
221 220 70 sstrdi fdom1gdom1ranfrang
222 i1f0rn fdom10ranf
223 elun1 0ranf0ranfrang
224 222 223 syl fdom10ranfrang
225 224 adantr fdom1gdom10ranfrang
226 ffn abs:absFn
227 35 226 ax-mp absFn
228 fnfvima absFnranfrang0ranfrang0absranfrang
229 227 228 mp3an1 ranfrang0ranfrang0absranfrang
230 221 225 229 syl2anc fdom1gdom10absranfrang
231 230 ne0d fdom1gdom1absranfrang
232 ffun abs:Funabs
233 35 232 ax-mp Funabs
234 i1frn fdom1ranfFin
235 i1frn gdom1rangFin
236 unfi ranfFinrangFinranfrangFin
237 234 235 236 syl2an fdom1gdom1ranfrangFin
238 imafi FunabsranfrangFinabsranfrangFin
239 233 237 238 sylancr fdom1gdom1absranfrangFin
240 fimaxre2 absranfrangabsranfrangFinxyabsranfrangyx
241 214 239 240 sylancr fdom1gdom1xyabsranfrangyx
242 suprcl absranfrangabsranfrangxyabsranfrangyxsupabsranfrang<
243 215 231 241 242 syl3anc fdom1gdom1supabsranfrang<
244 243 adantr fdom1gdom1rranfrangr0supabsranfrang<
245 0red fdom1gdom1rranfrangr00
246 221 sselda fdom1gdom1rranfrangr
247 246 abscld fdom1gdom1rranfrangr
248 247 adantrr fdom1gdom1rranfrangr0r
249 absgt0 rr00<r
250 246 249 syl fdom1gdom1rranfrangr00<r
251 250 biimpa fdom1gdom1rranfrangr00<r
252 251 anasss fdom1gdom1rranfrangr00<r
253 215 231 241 3jca fdom1gdom1absranfrangabsranfrangxyabsranfrangyx
254 253 adantr fdom1gdom1rranfrangabsranfrangabsranfrangxyabsranfrangyx
255 fnfvima absFnranfrangrranfrangrabsranfrang
256 227 255 mp3an1 ranfrangrranfrangrabsranfrang
257 221 256 sylan fdom1gdom1rranfrangrabsranfrang
258 suprub absranfrangabsranfrangxyabsranfrangyxrabsranfrangrsupabsranfrang<
259 254 257 258 syl2anc fdom1gdom1rranfrangrsupabsranfrang<
260 259 adantrr fdom1gdom1rranfrangr0rsupabsranfrang<
261 245 248 244 252 260 ltletrd fdom1gdom1rranfrangr00<supabsranfrang<
262 244 261 elrpd fdom1gdom1rranfrangr0supabsranfrang<+
263 262 rexlimdvaa fdom1gdom1rranfrangr0supabsranfrang<+
264 263 imp fdom1gdom1rranfrangr0supabsranfrang<+
265 rpmulcl 2+supabsranfrang<+2supabsranfrang<+
266 210 264 265 sylancr fdom1gdom1rranfrangr02supabsranfrang<+
267 209 266 rerpdivcld fdom1gdom1rranfrangr02tiftuwft+igt02supabsranfrang<
268 267 adantll φfdom1gdom1rranfrangr02tiftuwft+igt02supabsranfrang<
269 268 adantlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr02tiftuwft+igt02supabsranfrang<
270 269 ad3antrrr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt02supabsranfrang<
271 simp-4l φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+φ
272 iccssre ABAB
273 2 3 272 syl2anc φAB
274 273 70 sstrdi φAB
275 274 sselda φwABw
276 274 sselda φuABu
277 subcl wuwu
278 275 276 277 syl2anr φuABφwABwu
279 278 anandis φuABwABwu
280 279 abscld φuABwABwu
281 280 3adantr3 φuABwABuwwu
282 271 281 sylan φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu
283 282 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<wu
284 rpdivcl y2+2supabsranfrang<+y22supabsranfrang<+
285 155 266 284 syl2anr fdom1gdom1rranfrangr0y+y22supabsranfrang<+
286 285 rpred fdom1gdom1rranfrangr0y+y22supabsranfrang<
287 286 adantlll φfdom1gdom1rranfrangr0y+y22supabsranfrang<
288 287 adantllr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+y22supabsranfrang<
289 288 ad2antrr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<y22supabsranfrang<
290 273 sseld φuABu
291 273 sseld φwABw
292 idd φuwuw
293 290 291 292 3anim123d φuABwABuwuwuw
294 293 ad2antrr φfdom1gdom1rranfrangr0uABwABuwuwuw
295 294 imp φfdom1gdom1rranfrangr0uABwABuwuwuw
296 63 abscld fdom1gdom1tft+igt
297 296 rexrd fdom1gdom1tft+igt*
298 elxrge0 ft+igt0+∞ft+igt*0ft+igt
299 297 64 298 sylanbrc fdom1gdom1tft+igt0+∞
300 ifcl ft+igt0+∞00+∞iftuwft+igt00+∞
301 299 123 300 sylancl fdom1gdom1tiftuwft+igt00+∞
302 301 fmpttd fdom1gdom1tiftuwft+igt0:0+∞
303 243 recnd fdom1gdom1supabsranfrang<
304 303 2timesd fdom1gdom12supabsranfrang<=supabsranfrang<+supabsranfrang<
305 243 243 readdcld fdom1gdom1supabsranfrang<+supabsranfrang<
306 305 rexrd fdom1gdom1supabsranfrang<+supabsranfrang<*
307 abs0 0=0
308 307 230 eqeltrrid fdom1gdom10absranfrang
309 suprub absranfrangabsranfrangxyabsranfrangyx0absranfrang0supabsranfrang<
310 253 308 309 syl2anc fdom1gdom10supabsranfrang<
311 243 243 310 310 addge0d fdom1gdom10supabsranfrang<+supabsranfrang<
312 elxrge0 supabsranfrang<+supabsranfrang<0+∞supabsranfrang<+supabsranfrang<*0supabsranfrang<+supabsranfrang<
313 306 311 312 sylanbrc fdom1gdom1supabsranfrang<+supabsranfrang<0+∞
314 304 313 eqeltrd fdom1gdom12supabsranfrang<0+∞
315 ifcl 2supabsranfrang<0+∞00+∞iftuw2supabsranfrang<00+∞
316 314 123 315 sylancl fdom1gdom1iftuw2supabsranfrang<00+∞
317 316 adantr fdom1gdom1tiftuw2supabsranfrang<00+∞
318 317 fmpttd fdom1gdom1tiftuw2supabsranfrang<0:0+∞
319 9 ffvelrnda fdom1tft
320 319 recnd fdom1tft
321 320 abscld fdom1tft
322 13 ffvelrnda gdom1tgt
323 322 recnd gdom1tgt
324 323 abscld gdom1tgt
325 readdcl ftgtft+gt
326 321 324 325 syl2an fdom1tgdom1tft+gt
327 326 anandirs fdom1gdom1tft+gt
328 305 adantr fdom1gdom1tsupabsranfrang<+supabsranfrang<
329 mulcl igtigt
330 12 323 329 sylancr gdom1tigt
331 abstri ftigtft+igtft+igt
332 320 330 331 syl2an fdom1tgdom1tft+igtft+igt
333 332 anandirs fdom1gdom1tft+igtft+igt
334 absmul igtigt=igt
335 12 323 334 sylancr gdom1tigt=igt
336 absi i=1
337 336 oveq1i igt=1gt
338 335 337 eqtrdi gdom1tigt=1gt
339 324 recnd gdom1tgt
340 339 mulid2d gdom1t1gt=gt
341 338 340 eqtrd gdom1tigt=gt
342 341 adantll fdom1gdom1tigt=gt
343 342 oveq2d fdom1gdom1tft+igt=ft+gt
344 333 343 breqtrd fdom1gdom1tft+igtft+gt
345 321 adantlr fdom1gdom1tft
346 324 adantll fdom1gdom1tgt
347 243 adantr fdom1gdom1tsupabsranfrang<
348 253 adantr fdom1gdom1tabsranfrangabsranfrangxyabsranfrangyx
349 221 adantr fdom1gdom1tranfrang
350 9 ffnd fdom1fFn
351 fnfvelrn fFntftranf
352 350 351 sylan fdom1tftranf
353 elun1 ftranfftranfrang
354 352 353 syl fdom1tftranfrang
355 354 adantlr fdom1gdom1tftranfrang
356 fnfvima absFnranfrangftranfrangftabsranfrang
357 227 356 mp3an1 ranfrangftranfrangftabsranfrang
358 349 355 357 syl2anc fdom1gdom1tftabsranfrang
359 suprub absranfrangabsranfrangxyabsranfrangyxftabsranfrangftsupabsranfrang<
360 348 358 359 syl2anc fdom1gdom1tftsupabsranfrang<
361 13 ffnd gdom1gFn
362 fnfvelrn gFntgtrang
363 361 362 sylan gdom1tgtrang
364 elun2 gtranggtranfrang
365 363 364 syl gdom1tgtranfrang
366 365 adantll fdom1gdom1tgtranfrang
367 fnfvima absFnranfranggtranfranggtabsranfrang
368 227 367 mp3an1 ranfranggtranfranggtabsranfrang
369 349 366 368 syl2anc fdom1gdom1tgtabsranfrang
370 suprub absranfrangabsranfrangxyabsranfrangyxgtabsranfranggtsupabsranfrang<
371 348 369 370 syl2anc fdom1gdom1tgtsupabsranfrang<
372 345 346 347 347 360 371 le2addd fdom1gdom1tft+gtsupabsranfrang<+supabsranfrang<
373 296 327 328 344 372 letrd fdom1gdom1tft+igtsupabsranfrang<+supabsranfrang<
374 304 adantr fdom1gdom1t2supabsranfrang<=supabsranfrang<+supabsranfrang<
375 373 374 breqtrrd fdom1gdom1tft+igt2supabsranfrang<
376 58 375 sylan2 fdom1gdom1tuwft+igt2supabsranfrang<
377 iftrue tuwiftuwft+igt0=ft+igt
378 377 adantl fdom1gdom1tuwiftuwft+igt0=ft+igt
379 iftrue tuwiftuw2supabsranfrang<0=2supabsranfrang<
380 379 adantl fdom1gdom1tuwiftuw2supabsranfrang<0=2supabsranfrang<
381 376 378 380 3brtr4d fdom1gdom1tuwiftuwft+igt0iftuw2supabsranfrang<0
382 381 ex fdom1gdom1tuwiftuwft+igt0iftuw2supabsranfrang<0
383 66 a1i ¬tuw00
384 iffalse ¬tuwiftuwft+igt0=0
385 iffalse ¬tuwiftuw2supabsranfrang<0=0
386 383 384 385 3brtr4d ¬tuwiftuwft+igt0iftuw2supabsranfrang<0
387 382 386 pm2.61d1 fdom1gdom1iftuwft+igt0iftuw2supabsranfrang<0
388 387 ralrimivw fdom1gdom1tiftuwft+igt0iftuw2supabsranfrang<0
389 ovex 2supabsranfrang<V
390 389 72 ifex iftuw2supabsranfrang<0V
391 390 a1i fdom1gdom1tiftuw2supabsranfrang<0V
392 eqidd fdom1gdom1tiftuw2supabsranfrang<0=tiftuw2supabsranfrang<0
393 22 79 391 82 392 ofrfval2 fdom1gdom1tiftuwft+igt0ftiftuw2supabsranfrang<0tiftuwft+igt0iftuw2supabsranfrang<0
394 388 393 mpbird fdom1gdom1tiftuwft+igt0ftiftuw2supabsranfrang<0
395 itg2le tiftuwft+igt0:0+∞tiftuw2supabsranfrang<0:0+∞tiftuwft+igt0ftiftuw2supabsranfrang<02tiftuwft+igt02tiftuw2supabsranfrang<0
396 302 318 394 395 syl3anc fdom1gdom12tiftuwft+igt02tiftuw2supabsranfrang<0
397 396 adantr fdom1gdom1uwuw2tiftuwft+igt02tiftuw2supabsranfrang<0
398 mblvol uwdomvolvoluw=vol*uw
399 42 398 ax-mp voluw=vol*uw
400 ovolioo uwuwvol*uw=wu
401 399 400 eqtrid uwuwvoluw=wu
402 resubcl wuwu
403 402 ancoms uwwu
404 403 3adant3 uwuwwu
405 401 404 eqeltrd uwuwvoluw
406 elrege0 supabsranfrang<0+∞supabsranfrang<0supabsranfrang<
407 243 310 406 sylanbrc fdom1gdom1supabsranfrang<0+∞
408 ge0addcl supabsranfrang<0+∞supabsranfrang<0+∞supabsranfrang<+supabsranfrang<0+∞
409 407 407 408 syl2anc fdom1gdom1supabsranfrang<+supabsranfrang<0+∞
410 304 409 eqeltrd fdom1gdom12supabsranfrang<0+∞
411 itg2const uwdomvolvoluw2supabsranfrang<0+∞2tiftuw2supabsranfrang<0=2supabsranfrang<voluw
412 42 411 mp3an1 voluw2supabsranfrang<0+∞2tiftuw2supabsranfrang<0=2supabsranfrang<voluw
413 405 410 412 syl2anr fdom1gdom1uwuw2tiftuw2supabsranfrang<0=2supabsranfrang<voluw
414 397 413 breqtrd fdom1gdom1uwuw2tiftuwft+igt02supabsranfrang<voluw
415 414 adantll φfdom1gdom1uwuw2tiftuwft+igt02supabsranfrang<voluw
416 415 adantlr φfdom1gdom1rranfrangr0uwuw2tiftuwft+igt02supabsranfrang<voluw
417 90 ad3antlr φfdom1gdom1rranfrangr0uwuw2tiftuwft+igt0
418 405 adantl φfdom1gdom1rranfrangr0uwuwvoluw
419 266 adantll φfdom1gdom1rranfrangr02supabsranfrang<+
420 419 adantr φfdom1gdom1rranfrangr0uwuw2supabsranfrang<+
421 417 418 420 ledivmuld φfdom1gdom1rranfrangr0uwuw2tiftuwft+igt02supabsranfrang<voluw2tiftuwft+igt02supabsranfrang<voluw
422 416 421 mpbird φfdom1gdom1rranfrangr0uwuw2tiftuwft+igt02supabsranfrang<voluw
423 abssubge0 uwuwwu=wu
424 400 423 eqtr4d uwuwvol*uw=wu
425 399 424 eqtrid uwuwvoluw=wu
426 425 adantl φfdom1gdom1rranfrangr0uwuwvoluw=wu
427 422 426 breqtrd φfdom1gdom1rranfrangr0uwuw2tiftuwft+igt02supabsranfrang<wu
428 295 427 syldan φfdom1gdom1rranfrangr0uABwABuw2tiftuwft+igt02supabsranfrang<wu
429 428 adantllr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0uABwABuw2tiftuwft+igt02supabsranfrang<wu
430 429 adantlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuw2tiftuwft+igt02supabsranfrang<wu
431 430 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt02supabsranfrang<wu
432 simpr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<wu<y22supabsranfrang<
433 270 283 289 431 432 lelttrd φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt02supabsranfrang<<y22supabsranfrang<
434 90 adantl φfdom1gdom12tiftuwft+igt0
435 434 ad3antrrr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+2tiftuwft+igt0
436 130 adantl φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+y2
437 419 adantlr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr02supabsranfrang<+
438 437 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+2supabsranfrang<+
439 435 436 438 ltdiv1d φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+2tiftuwft+igt0<y22tiftuwft+igt02supabsranfrang<<y22supabsranfrang<
440 439 ad2antrr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0<y22tiftuwft+igt02supabsranfrang<<y22supabsranfrang<
441 433 440 mpbird φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0<y2
442 201 adantllr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwAB2tiftuwFtft+igt0<y2
443 442 3adantr3 φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuw2tiftuwFtft+igt0<y2
444 443 adantr φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwFtft+igt0<y2
445 91 207 208 208 441 444 lt2addd φfdom1gdom12tiftDFt0ft+igt<y2rranfrangr0y+uABwABuwwu<y22supabsranfrang<2tiftuwft+igt0+2tiftuwFtft+igt0<y2+y2