Metamath Proof Explorer


Theorem itg2addnclem

Description: An alternate expression for the S.2 integral that includes an arbitrarily small but strictly positive "buffer zone" wherever the simple function is nonzero. (Contributed by Brendan Leahy, 10-Oct-2017) (Revised by Brendan Leahy, 10-Mar-2018)

Ref Expression
Hypothesis itg2addnclem.1 L=x|gdom1y+zifgz=00gz+yfFx=1g
Assertion itg2addnclem F:0+∞2F=supL*<

Proof

Step Hyp Ref Expression
1 itg2addnclem.1 L=x|gdom1y+zifgz=00gz+yfFx=1g
2 eqid x|fdom1ffFx=1f=x|fdom1ffFx=1f
3 2 itg2val F:0+∞2F=supx|fdom1ffFx=1f*<
4 1 supeq1i supL*<=supx|gdom1y+zifgz=00gz+yfFx=1g*<
5 xrltso <Or*
6 5 a1i F:0+∞<Or*
7 simprr fdom1ffFx=1fx=1f
8 itg1cl fdom11f
9 8 rexrd fdom11f*
10 9 adantr fdom1ffFx=1f1f*
11 7 10 eqeltrd fdom1ffFx=1fx*
12 11 rexlimiva fdom1ffFx=1fx*
13 12 abssi x|fdom1ffFx=1f*
14 supxrcl x|fdom1ffFx=1f*supx|fdom1ffFx=1f*<*
15 13 14 mp1i F:0+∞supx|fdom1ffFx=1f*<*
16 fveq1 g=fgz=fz
17 16 eqeq1d g=fgz=0fz=0
18 16 oveq1d g=fgz+y=fz+y
19 17 18 ifbieq2d g=fifgz=00gz+y=iffz=00fz+y
20 19 mpteq2dv g=fzifgz=00gz+y=ziffz=00fz+y
21 20 breq1d g=fzifgz=00gz+yfFziffz=00fz+yfF
22 21 rexbidv g=fy+zifgz=00gz+yfFy+ziffz=00fz+yfF
23 fveq2 g=f1g=1f
24 23 eqeq2d g=fx=1gx=1f
25 22 24 anbi12d g=fy+zifgz=00gz+yfFx=1gy+ziffz=00fz+yfFx=1f
26 25 cbvrexvw gdom1y+zifgz=00gz+yfFx=1gfdom1y+ziffz=00fz+yfFx=1f
27 breq2 0=iffz=00fz+yfz0fziffz=00fz+y
28 breq2 fz+y=iffz=00fz+yfzfz+yfziffz=00fz+y
29 id fz=0fz=0
30 0le0 00
31 29 30 eqbrtrdi fz=0fz0
32 31 adantl fdom1y+zfz=0fz0
33 rpge0 y+0y
34 33 ad2antlr fdom1y+z0y
35 i1ff fdom1f:
36 35 ffvelcdmda fdom1zfz
37 36 adantlr fdom1y+zfz
38 rpre y+y
39 38 ad2antlr fdom1y+zy
40 37 39 addge01d fdom1y+z0yfzfz+y
41 34 40 mpbid fdom1y+zfzfz+y
42 41 adantr fdom1y+z¬fz=0fzfz+y
43 27 28 32 42 ifbothda fdom1y+zfziffz=00fz+y
44 43 adantlll F:0+∞fdom1y+zfziffz=00fz+y
45 35 ad2antlr F:0+∞fdom1y+f:
46 45 ffvelcdmda F:0+∞fdom1y+zfz
47 46 rexrd F:0+∞fdom1y+zfz*
48 0re 0
49 38 ad2antlr F:0+∞fdom1y+zy
50 46 49 readdcld F:0+∞fdom1y+zfz+y
51 ifcl 0fz+yiffz=00fz+y
52 48 50 51 sylancr F:0+∞fdom1y+ziffz=00fz+y
53 52 rexrd F:0+∞fdom1y+ziffz=00fz+y*
54 iccssxr 0+∞*
55 fss F:0+∞0+∞*F:*
56 54 55 mpan2 F:0+∞F:*
57 56 ad2antrr F:0+∞fdom1y+F:*
58 57 ffvelcdmda F:0+∞fdom1y+zFz*
59 xrletr fz*iffz=00fz+y*Fz*fziffz=00fz+yiffz=00fz+yFzfzFz
60 47 53 58 59 syl3anc F:0+∞fdom1y+zfziffz=00fz+yiffz=00fz+yFzfzFz
61 44 60 mpand F:0+∞fdom1y+ziffz=00fz+yFzfzFz
62 61 ralimdva F:0+∞fdom1y+ziffz=00fz+yFzzfzFz
63 reex V
64 63 a1i F:0+∞fdom1y+V
65 eqidd F:0+∞fdom1y+ziffz=00fz+y=ziffz=00fz+y
66 id F:0+∞F:0+∞
67 66 feqmptd F:0+∞F=zFz
68 67 ad2antrr F:0+∞fdom1y+F=zFz
69 64 52 58 65 68 ofrfval2 F:0+∞fdom1y+ziffz=00fz+yfFziffz=00fz+yFz
70 35 feqmptd fdom1f=zfz
71 70 ad2antlr F:0+∞fdom1y+f=zfz
72 64 46 58 71 68 ofrfval2 F:0+∞fdom1y+ffFzfzFz
73 62 69 72 3imtr4d F:0+∞fdom1y+ziffz=00fz+yfFffF
74 73 rexlimdva F:0+∞fdom1y+ziffz=00fz+yfFffF
75 74 anim1d F:0+∞fdom1y+ziffz=00fz+yfFx=1fffFx=1f
76 75 reximdva F:0+∞fdom1y+ziffz=00fz+yfFx=1ffdom1ffFx=1f
77 26 76 biimtrid F:0+∞gdom1y+zifgz=00gz+yfFx=1gfdom1ffFx=1f
78 77 ss2abdv F:0+∞x|gdom1y+zifgz=00gz+yfFx=1gx|fdom1ffFx=1f
79 78 sseld F:0+∞bx|gdom1y+zifgz=00gz+yfFx=1gbx|fdom1ffFx=1f
80 simp3r F:0+∞fdom1ffFx=1fx=1f
81 9 3ad2ant2 F:0+∞fdom1ffFx=1f1f*
82 80 81 eqeltrd F:0+∞fdom1ffFx=1fx*
83 82 rexlimdv3a F:0+∞fdom1ffFx=1fx*
84 83 abssdv F:0+∞x|fdom1ffFx=1f*
85 xrsupss x|fdom1ffFx=1f*a*bx|fdom1ffFx=1f¬a<bb*b<asx|fdom1ffFx=1fb<s
86 84 85 syl F:0+∞a*bx|fdom1ffFx=1f¬a<bb*b<asx|fdom1ffFx=1fb<s
87 6 86 supub F:0+∞bx|fdom1ffFx=1f¬supx|fdom1ffFx=1f*<<b
88 79 87 syld F:0+∞bx|gdom1y+zifgz=00gz+yfFx=1g¬supx|fdom1ffFx=1f*<<b
89 88 imp F:0+∞bx|gdom1y+zifgz=00gz+yfFx=1g¬supx|fdom1ffFx=1f*<<b
90 supxrlub x|fdom1ffFx=1f*b*b<supx|fdom1ffFx=1f*<sx|fdom1ffFx=1fb<s
91 13 90 mpan b*b<supx|fdom1ffFx=1f*<sx|fdom1ffFx=1fb<s
92 91 adantl F:0+∞b*b<supx|fdom1ffFx=1f*<sx|fdom1ffFx=1fb<s
93 simprrr F:0+∞b*fdom1ffFs=1fs=1f
94 93 breq2d F:0+∞b*fdom1ffFs=1fb<sb<1f
95 simplll F:0+∞b*fdom1ffFs=1fb<1fF:0+∞
96 i1f0 ×0dom1
97 2rp 2+
98 97 ne0ii +
99 ffvelcdm F:0+∞zFz0+∞
100 elxrge0 Fz0+∞Fz*0Fz
101 99 100 sylib F:0+∞zFz*0Fz
102 101 simprd F:0+∞z0Fz
103 102 ralrimiva F:0+∞z0Fz
104 63 a1i F:0+∞V
105 c0ex 0V
106 105 a1i F:0+∞z0V
107 eqidd F:0+∞z0=z0
108 104 106 99 107 67 ofrfval2 F:0+∞z0fFz0Fz
109 103 108 mpbird F:0+∞z0fF
110 109 ralrimivw F:0+∞y+z0fF
111 r19.2z +y+z0fFy+z0fF
112 98 110 111 sylancr F:0+∞y+z0fF
113 fveq2 g=×01g=1×0
114 itg10 1×0=0
115 113 114 eqtr2di g=×00=1g
116 115 biantrud g=×0y+zifgz=00gz+yfFy+zifgz=00gz+yfF0=1g
117 fveq1 g=×0gz=×0z
118 105 fvconst2 z×0z=0
119 117 118 sylan9eq g=×0zgz=0
120 iftrue gz=0ifgz=00gz+y=0
121 119 120 syl g=×0zifgz=00gz+y=0
122 121 mpteq2dva g=×0zifgz=00gz+y=z0
123 122 breq1d g=×0zifgz=00gz+yfFz0fF
124 123 rexbidv g=×0y+zifgz=00gz+yfFy+z0fF
125 116 124 bitr3d g=×0y+zifgz=00gz+yfF0=1gy+z0fF
126 125 rspcev ×0dom1y+z0fFgdom1y+zifgz=00gz+yfF0=1g
127 96 112 126 sylancr F:0+∞gdom1y+zifgz=00gz+yfF0=1g
128 id b=−∞b=−∞
129 mnflt 0−∞<0
130 48 129 mp1i b=−∞−∞<0
131 128 130 eqbrtrd b=−∞b<0
132 eqeq1 a=0a=1g0=1g
133 132 anbi2d a=0y+zifgz=00gz+yfFa=1gy+zifgz=00gz+yfF0=1g
134 133 rexbidv a=0gdom1y+zifgz=00gz+yfFa=1ggdom1y+zifgz=00gz+yfF0=1g
135 breq2 a=0b<ab<0
136 134 135 anbi12d a=0gdom1y+zifgz=00gz+yfFa=1gb<agdom1y+zifgz=00gz+yfF0=1gb<0
137 105 136 spcev gdom1y+zifgz=00gz+yfF0=1gb<0agdom1y+zifgz=00gz+yfFa=1gb<a
138 127 131 137 syl2an F:0+∞b=−∞agdom1y+zifgz=00gz+yfFa=1gb<a
139 95 138 sylan F:0+∞b*fdom1ffFs=1fb<1fb=−∞agdom1y+zifgz=00gz+yfFa=1gb<a
140 simp-4r F:0+∞b*fdom1ffFs=1fb<1fb−∞b*
141 8 adantr fdom1ffFs=1f1f
142 141 ad3antlr F:0+∞b*fdom1ffFs=1fb<1fb−∞1f
143 simpllr F:0+∞b*fdom1ffFs=1fb<1fb*
144 ngtmnft b*b=−∞¬−∞<b
145 144 biimprd b*¬−∞<bb=−∞
146 145 necon1ad b*b−∞−∞<b
147 146 imp b*b−∞−∞<b
148 143 147 sylan F:0+∞b*fdom1ffFs=1fb<1fb−∞−∞<b
149 simpr F:0+∞b*b*
150 9 adantr fdom1ffFs=1f1f*
151 149 150 anim12i F:0+∞b*fdom1ffFs=1fb*1f*
152 xrltle b*1f*b<1fb1f
153 152 imp b*1f*b<1fb1f
154 151 153 sylan F:0+∞b*fdom1ffFs=1fb<1fb1f
155 154 adantr F:0+∞b*fdom1ffFs=1fb<1fb−∞b1f
156 xrre b*1f−∞<bb1fb
157 140 142 148 155 156 syl22anc F:0+∞b*fdom1ffFs=1fb<1fb−∞b
158 127 ad3antrrr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf0=0gdom1y+zifgz=00gz+yfF0=1g
159 simplrl F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf0=0b<1f
160 simplrl F:0+∞fdom1ffFs=1fb<1fbfdom1
161 simpl fdom1vol*f-1ranf0=0fdom1
162 cnvimass f-1ranf0domf
163 162 35 fssdm fdom1f-1ranf0
164 163 adantr fdom1vol*f-1ranf0=0f-1ranf0
165 simpr fdom1vol*f-1ranf0=0vol*f-1ranf0=0
166 fdm f:domf=
167 166 eqcomd f:=domf
168 ffun f:Funf
169 difpreima Funff-1ranf0=f-1ranff-10
170 168 169 syl f:f-1ranf0=f-1ranff-10
171 cnvimarndm f-1ranf=domf
172 171 difeq1i f-1ranff-10=domff-10
173 170 172 eqtrdi f:f-1ranf0=domff-10
174 167 173 difeq12d f:f-1ranf0=domfdomff-10
175 cnvimass f-10domf
176 dfss4 f-10domfdomfdomff-10=f-10
177 175 176 mpbi domfdomff-10=f-10
178 174 177 eqtrdi f:f-1ranf0=f-10
179 178 eleq2d f:zf-1ranf0zf-10
180 ffn f:fFn
181 fniniseg fFnzf-10zfz=0
182 simpr zfz=0fz=0
183 181 182 syl6bi fFnzf-10fz=0
184 180 183 syl f:zf-10fz=0
185 179 184 sylbid f:zf-1ranf0fz=0
186 35 185 syl fdom1zf-1ranf0fz=0
187 186 imp fdom1zf-1ranf0fz=0
188 187 adantlr fdom1vol*f-1ranf0=0zf-1ranf0fz=0
189 161 164 165 188 itg10a fdom1vol*f-1ranf0=01f=0
190 160 189 sylan F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf0=01f=0
191 159 190 breqtrd F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf0=0b<0
192 158 191 137 syl2anc F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf0=0agdom1y+zifgz=00gz+yfFa=1gb<a
193 simprl F:0+∞fdom1ffFs=1ffdom1
194 simpr b<1fbb
195 193 194 anim12i F:0+∞fdom1ffFs=1fb<1fbfdom1b
196 63 a1i fdom1bvol*f-1ranf00V
197 fvex fuV
198 197 a1i fdom1bvol*f-1ranf00ufuV
199 ovex 1fb2vol*f-1ranf0V
200 199 105 ifex ifuf-1ranf01fb2vol*f-1ranf00V
201 200 a1i fdom1bvol*f-1ranf00uifuf-1ranf01fb2vol*f-1ranf00V
202 35 feqmptd fdom1f=ufu
203 202 ad2antrr fdom1bvol*f-1ranf00f=ufu
204 eqidd fdom1bvol*f-1ranf00uifuf-1ranf01fb2vol*f-1ranf00=uifuf-1ranf01fb2vol*f-1ranf00
205 196 198 201 203 204 offval2 fdom1bvol*f-1ranf00ffuifuf-1ranf01fb2vol*f-1ranf00=ufuifuf-1ranf01fb2vol*f-1ranf00
206 ovif2 fuifuf-1ranf01fb2vol*f-1ranf00=ifuf-1ranf0fu1fb2vol*f-1ranf0fu0
207 171 166 eqtrid f:f-1ranf=
208 207 difeq1d f:f-1ranff-10=f-10
209 170 208 eqtrd f:f-1ranf0=f-10
210 209 eleq2d f:uf-1ranf0uf-10
211 35 210 syl fdom1uf-1ranf0uf-10
212 211 ad3antrrr fdom1bvol*f-1ranf00uuf-1ranf0uf-10
213 simpr fdom1bvol*f-1ranf00uu
214 213 biantrurd fdom1bvol*f-1ranf00u¬uf-10u¬uf-10
215 eldif uf-10u¬uf-10
216 214 215 bitr4di fdom1bvol*f-1ranf00u¬uf-10uf-10
217 212 216 bitr4d fdom1bvol*f-1ranf00uuf-1ranf0¬uf-10
218 217 con2bid fdom1bvol*f-1ranf00uuf-10¬uf-1ranf0
219 fniniseg fFnuf-10ufu=0
220 35 180 219 3syl fdom1uf-10ufu=0
221 220 ad3antrrr fdom1bvol*f-1ranf00uuf-10ufu=0
222 218 221 bitr3d fdom1bvol*f-1ranf00u¬uf-1ranf0ufu=0
223 oveq1 fu=0fu0=00
224 0m0e0 00=0
225 223 224 eqtrdi fu=0fu0=0
226 225 adantl ufu=0fu0=0
227 222 226 syl6bi fdom1bvol*f-1ranf00u¬uf-1ranf0fu0=0
228 227 imp fdom1bvol*f-1ranf00u¬uf-1ranf0fu0=0
229 228 ifeq2da fdom1bvol*f-1ranf00uifuf-1ranf0fu1fb2vol*f-1ranf0fu0=ifuf-1ranf0fu1fb2vol*f-1ranf00
230 206 229 eqtrid fdom1bvol*f-1ranf00ufuifuf-1ranf01fb2vol*f-1ranf00=ifuf-1ranf0fu1fb2vol*f-1ranf00
231 230 mpteq2dva fdom1bvol*f-1ranf00ufuifuf-1ranf01fb2vol*f-1ranf00=uifuf-1ranf0fu1fb2vol*f-1ranf00
232 205 231 eqtrd fdom1bvol*f-1ranf00ffuifuf-1ranf01fb2vol*f-1ranf00=uifuf-1ranf0fu1fb2vol*f-1ranf00
233 simpll fdom1bvol*f-1ranf00fdom1
234 199 a1i fdom1bvol*f-1ranf00u1fb2vol*f-1ranf0V
235 1ex 1V
236 235 105 ifex ifuf-1ranf010V
237 236 a1i fdom1bvol*f-1ranf00uifuf-1ranf010V
238 fconstmpt ×1fb2vol*f-1ranf0=u1fb2vol*f-1ranf0
239 238 a1i fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0=u1fb2vol*f-1ranf0
240 eqidd fdom1bvol*f-1ranf00uifuf-1ranf010=uifuf-1ranf010
241 196 234 237 239 240 offval2 fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fuifuf-1ranf010=u1fb2vol*f-1ranf0ifuf-1ranf010
242 ovif2 1fb2vol*f-1ranf0ifuf-1ranf010=ifuf-1ranf01fb2vol*f-1ranf011fb2vol*f-1ranf00
243 resubcl 1fb1fb
244 8 243 sylan fdom1b1fb
245 244 adantr fdom1bvol*f-1ranf001fb
246 2re 2
247 i1fima fdom1f-1ranf0domvol
248 mblvol f-1ranf0domvolvolf-1ranf0=vol*f-1ranf0
249 247 248 syl fdom1volf-1ranf0=vol*f-1ranf0
250 neldifsn ¬0ranf0
251 i1fima2 fdom1¬0ranf0volf-1ranf0
252 250 251 mpan2 fdom1volf-1ranf0
253 249 252 eqeltrrd fdom1vol*f-1ranf0
254 remulcl 2vol*f-1ranf02vol*f-1ranf0
255 246 253 254 sylancr fdom12vol*f-1ranf0
256 255 ad2antrr fdom1bvol*f-1ranf002vol*f-1ranf0
257 2cnd fdom1bvol*f-1ranf002
258 253 ad2antrr fdom1bvol*f-1ranf00vol*f-1ranf0
259 258 recnd fdom1bvol*f-1ranf00vol*f-1ranf0
260 2ne0 20
261 260 a1i fdom1bvol*f-1ranf0020
262 simpr fdom1bvol*f-1ranf00vol*f-1ranf00
263 257 259 261 262 mulne0d fdom1bvol*f-1ranf002vol*f-1ranf00
264 245 256 263 redivcld fdom1bvol*f-1ranf001fb2vol*f-1ranf0
265 264 recnd fdom1bvol*f-1ranf001fb2vol*f-1ranf0
266 265 mulridd fdom1bvol*f-1ranf001fb2vol*f-1ranf01=1fb2vol*f-1ranf0
267 265 mul01d fdom1bvol*f-1ranf001fb2vol*f-1ranf00=0
268 266 267 ifeq12d fdom1bvol*f-1ranf00ifuf-1ranf01fb2vol*f-1ranf011fb2vol*f-1ranf00=ifuf-1ranf01fb2vol*f-1ranf00
269 242 268 eqtrid fdom1bvol*f-1ranf001fb2vol*f-1ranf0ifuf-1ranf010=ifuf-1ranf01fb2vol*f-1ranf00
270 269 mpteq2dv fdom1bvol*f-1ranf00u1fb2vol*f-1ranf0ifuf-1ranf010=uifuf-1ranf01fb2vol*f-1ranf00
271 241 270 eqtrd fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fuifuf-1ranf010=uifuf-1ranf01fb2vol*f-1ranf00
272 eqid uifuf-1ranf010=uifuf-1ranf010
273 272 i1f1 f-1ranf0domvolvolf-1ranf0uifuf-1ranf010dom1
274 247 252 273 syl2anc fdom1uifuf-1ranf010dom1
275 274 ad2antrr fdom1bvol*f-1ranf00uifuf-1ranf010dom1
276 275 264 i1fmulc fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fuifuf-1ranf010dom1
277 271 276 eqeltrrd fdom1bvol*f-1ranf00uifuf-1ranf01fb2vol*f-1ranf00dom1
278 i1fsub fdom1uifuf-1ranf01fb2vol*f-1ranf00dom1ffuifuf-1ranf01fb2vol*f-1ranf00dom1
279 233 277 278 syl2anc fdom1bvol*f-1ranf00ffuifuf-1ranf01fb2vol*f-1ranf00dom1
280 232 279 eqeltrrd fdom1bvol*f-1ranf00uifuf-1ranf0fu1fb2vol*f-1ranf00dom1
281 iftrue 0fz1fb2vol*f-1ranf0zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=fz1fb2vol*f-1ranf0
282 iftrue zf-1ranf0ifzf-1ranf0fz1fb2vol*f-1ranf00=fz1fb2vol*f-1ranf0
283 282 breq2d zf-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000fz1fb2vol*f-1ranf0
284 283 282 ifbieq1d zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
285 iftrue 0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00=fz1fb2vol*f-1ranf0
286 284 285 sylan9eqr 0fz1fb2vol*f-1ranf0zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=fz1fb2vol*f-1ranf0
287 281 286 eqtr4d 0fz1fb2vol*f-1ranf0zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000
288 iffalse ¬0fz1fb2vol*f-1ranf0zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0
289 ianor ¬0fz1fb2vol*f-1ranf0zf-1ranf0¬0fz1fb2vol*f-1ranf0¬zf-1ranf0
290 283 ifbid zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=if0fz1fb2vol*f-1ranf0ifzf-1ranf0fz1fb2vol*f-1ranf000
291 iffalse ¬0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0ifzf-1ranf0fz1fb2vol*f-1ranf000=0
292 290 291 sylan9eqr ¬0fz1fb2vol*f-1ranf0zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
293 292 ex ¬0fz1fb2vol*f-1ranf0zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
294 iffalse ¬zf-1ranf0ifzf-1ranf0fz1fb2vol*f-1ranf00=0
295 eqid 0=0
296 eqeq1 ifzf-1ranf0fz1fb2vol*f-1ranf00=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000ifzf-1ranf0fz1fb2vol*f-1ranf00=0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
297 eqeq1 0=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf0000=0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
298 296 297 ifboth ifzf-1ranf0fz1fb2vol*f-1ranf00=00=0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
299 294 295 298 sylancl ¬zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
300 293 299 pm2.61d1 ¬0fz1fb2vol*f-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
301 300 299 jaoi ¬0fz1fb2vol*f-1ranf0¬zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
302 289 301 sylbi ¬0fz1fb2vol*f-1ranf0zf-1ranf0if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000=0
303 288 302 eqtr4d ¬0fz1fb2vol*f-1ranf0zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000
304 287 303 pm2.61i if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000
305 eleq1w u=zuf-1ranf0zf-1ranf0
306 fveq2 u=zfu=fz
307 306 oveq1d u=zfu1fb2vol*f-1ranf0=fz1fb2vol*f-1ranf0
308 305 307 ifbieq1d u=zifuf-1ranf0fu1fb2vol*f-1ranf00=ifzf-1ranf0fz1fb2vol*f-1ranf00
309 eqid uifuf-1ranf0fu1fb2vol*f-1ranf00=uifuf-1ranf0fu1fb2vol*f-1ranf00
310 ovex fz1fb2vol*f-1ranf0V
311 310 105 ifex ifzf-1ranf0fz1fb2vol*f-1ranf00V
312 308 309 311 fvmpt zuifuf-1ranf0fu1fb2vol*f-1ranf00z=ifzf-1ranf0fz1fb2vol*f-1ranf00
313 312 breq2d z0uifuf-1ranf0fu1fb2vol*f-1ranf00z0ifzf-1ranf0fz1fb2vol*f-1ranf00
314 313 312 ifbieq1d zif0uifuf-1ranf0fu1fb2vol*f-1ranf00zuifuf-1ranf0fu1fb2vol*f-1ranf00z0=if0ifzf-1ranf0fz1fb2vol*f-1ranf00ifzf-1ranf0fz1fb2vol*f-1ranf000
315 304 314 eqtr4id zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=if0uifuf-1ranf0fu1fb2vol*f-1ranf00zuifuf-1ranf0fu1fb2vol*f-1ranf00z0
316 315 mpteq2ia zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=zif0uifuf-1ranf0fu1fb2vol*f-1ranf00zuifuf-1ranf0fu1fb2vol*f-1ranf00z0
317 316 i1fpos uifuf-1ranf0fu1fb2vol*f-1ranf00dom1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1
318 280 317 syl fdom1bvol*f-1ranf00zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1
319 195 318 sylan F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1
320 195 264 sylan F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf001fb2vol*f-1ranf0
321 8 ad2antrl F:0+∞fdom1ffFs=1f1f
322 321 194 243 syl2an F:0+∞fdom1ffFs=1fb<1fb1fb
323 322 adantr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf001fb
324 255 adantr fdom1ffFs=1f2vol*f-1ranf0
325 324 ad3antlr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf002vol*f-1ranf0
326 simprl F:0+∞fdom1ffFs=1fb<1fbb<1f
327 simprr F:0+∞fdom1ffFs=1fb<1fbb
328 141 ad2antlr F:0+∞fdom1ffFs=1fb<1fb1f
329 327 328 posdifd F:0+∞fdom1ffFs=1fb<1fbb<1f0<1fb
330 326 329 mpbid F:0+∞fdom1ffFs=1fb<1fb0<1fb
331 330 adantr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf000<1fb
332 253 adantr fdom1ffFs=1fvol*f-1ranf0
333 332 ad3antlr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00vol*f-1ranf0
334 mblss f-1ranf0domvolf-1ranf0
335 ovolge0 f-1ranf00vol*f-1ranf0
336 247 334 335 3syl fdom10vol*f-1ranf0
337 ltlen 0vol*f-1ranf00<vol*f-1ranf00vol*f-1ranf0vol*f-1ranf00
338 48 253 337 sylancr fdom10<vol*f-1ranf00vol*f-1ranf0vol*f-1ranf00
339 338 biimprd fdom10vol*f-1ranf0vol*f-1ranf000<vol*f-1ranf0
340 336 339 mpand fdom1vol*f-1ranf000<vol*f-1ranf0
341 340 ad2antrl F:0+∞fdom1ffFs=1fvol*f-1ranf000<vol*f-1ranf0
342 341 imp F:0+∞fdom1ffFs=1fvol*f-1ranf000<vol*f-1ranf0
343 342 adantlr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf000<vol*f-1ranf0
344 2pos 0<2
345 mulgt0 20<2vol*f-1ranf00<vol*f-1ranf00<2vol*f-1ranf0
346 246 344 345 mpanl12 vol*f-1ranf00<vol*f-1ranf00<2vol*f-1ranf0
347 333 343 346 syl2anc F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf000<2vol*f-1ranf0
348 323 325 331 347 divgt0d F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf000<1fb2vol*f-1ranf0
349 320 348 elrpd F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf001fb2vol*f-1ranf0+
350 simprl fdom1ffFs=1fffF
351 350 ad3antlr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00ffF
352 ffn F:0+∞FFn
353 35 180 syl fdom1fFn
354 353 adantr fdom1ffFs=1ffFn
355 simpr FFnfFnfFn
356 simpl FFnfFnFFn
357 63 a1i FFnfFnV
358 inidm =
359 eqidd FFnfFnzfz=fz
360 eqidd FFnfFnzFz=Fz
361 355 356 357 357 358 359 360 ofrfval FFnfFnffFzfzFz
362 352 354 361 syl2an F:0+∞fdom1ffFs=1fffFzfzFz
363 362 ad2antrr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00ffFzfzFz
364 simpl fdom1ffFs=1ffdom1
365 364 anim2i F:0+∞fdom1ffFs=1fF:0+∞fdom1
366 365 194 anim12i F:0+∞fdom1ffFs=1fb<1fbF:0+∞fdom1b
367 breq1 0=ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf00Fzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
368 breq1 if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0=ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
369 simplll F:0+∞fdom1bvol*f-1ranf00F:0+∞
370 369 ffvelcdmda F:0+∞fdom1bvol*f-1ranf00zFz0+∞
371 370 100 sylib F:0+∞fdom1bvol*f-1ranf00zFz*0Fz
372 371 simprd F:0+∞fdom1bvol*f-1ranf00z0Fz
373 372 ad2antrr F:0+∞fdom1bvol*f-1ranf00zfzFzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00Fz
374 oveq1 fz1fb2vol*f-1ranf0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
375 374 breq1d fz1fb2vol*f-1ranf0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0Fzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
376 oveq1 0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf000+1fb2vol*f-1ranf0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
377 376 breq1d 0=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf000+1fb2vol*f-1ranf0Fzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
378 35 ad3antlr F:0+∞fdom1bvol*f-1ranf00f:
379 378 ffvelcdmda F:0+∞fdom1bvol*f-1ranf00zfz
380 379 recnd F:0+∞fdom1bvol*f-1ranf00zfz
381 244 recnd fdom1b1fb
382 381 adantr fdom1bvol*f-1ranf001fb
383 255 recnd fdom12vol*f-1ranf0
384 383 ad2antrr fdom1bvol*f-1ranf002vol*f-1ranf0
385 382 384 263 divcld fdom1bvol*f-1ranf001fb2vol*f-1ranf0
386 385 adantlll F:0+∞fdom1bvol*f-1ranf001fb2vol*f-1ranf0
387 386 adantr F:0+∞fdom1bvol*f-1ranf00z1fb2vol*f-1ranf0
388 380 387 npcand F:0+∞fdom1bvol*f-1ranf00zfz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0=fz
389 388 adantr F:0+∞fdom1bvol*f-1ranf00zfzFzfz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0=fz
390 simpr F:0+∞fdom1bvol*f-1ranf00zfzFzfzFz
391 389 390 eqbrtrd F:0+∞fdom1bvol*f-1ranf00zfzFzfz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0Fz
392 391 ad2antrr F:0+∞fdom1bvol*f-1ranf00zfzFz¬if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00fz1fb2vol*f-1ranf0zf-1ranf0fz-1fb2vol*f-1ranf0+1fb2vol*f-1ranf0Fz
393 288 pm2.24d ¬0fz1fb2vol*f-1ranf0zf-1ranf0¬if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00+1fb2vol*f-1ranf0Fz
394 393 impcom ¬if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0¬0fz1fb2vol*f-1ranf0zf-1ranf00+1fb2vol*f-1ranf0Fz
395 394 adantll F:0+∞fdom1bvol*f-1ranf00zfzFz¬if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0¬0fz1fb2vol*f-1ranf0zf-1ranf00+1fb2vol*f-1ranf0Fz
396 375 377 392 395 ifbothda F:0+∞fdom1bvol*f-1ranf00zfzFz¬if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
397 367 368 373 396 ifbothda F:0+∞fdom1bvol*f-1ranf00zfzFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
398 397 ex F:0+∞fdom1bvol*f-1ranf00zfzFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
399 366 398 sylanl1 F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zfzFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
400 399 ralimdva F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zfzFzzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
401 363 400 sylbid F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00ffFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
402 351 401 mpd F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
403 ovex if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0V
404 105 403 ifex ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0V
405 404 a1i F:0+∞zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0V
406 eqidd F:0+∞zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0=zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
407 104 405 99 406 67 ofrfval2 F:0+∞zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0fFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
408 407 ad3antrrr F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0fFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0Fz
409 402 408 mpbird F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0fF
410 oveq2 y=1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
411 410 ifeq2d y=1fb2vol*f-1ranf0ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y=ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
412 411 mpteq2dv y=1fb2vol*f-1ranf0zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y=zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0
413 412 breq1d y=1fb2vol*f-1ranf0zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0fF
414 413 rspcev 1fb2vol*f-1ranf0+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+1fb2vol*f-1ranf0fFy+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfF
415 349 409 414 syl2anc F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00y+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfF
416 fveq2 zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=g1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
417 416 eqcoms g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf001zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
418 417 biantrud g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00y+zifgz=00gz+yfFy+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
419 nfmpt1 _zzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
420 419 nfeq2 zg=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
421 fveq1 g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00gz=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00z
422 310 105 ifex if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00V
423 eqid zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
424 423 fvmpt2 zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00Vzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00z=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
425 422 424 mpan2 zzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00z=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
426 421 425 sylan9eq g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zgz=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
427 426 eqeq1d g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zgz=0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0
428 426 oveq1d g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zgz+y=if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y
429 427 428 ifbieq2d g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zifgz=00gz+y=ifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y
430 420 429 mpteq2da g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zifgz=00gz+y=zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+y
431 430 breq1d g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zifgz=00gz+yfFzifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfF
432 431 rexbidv g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00y+zifgz=00gz+yfFy+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfF
433 418 432 bitr3d g=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1gy+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfF
434 433 rspcev zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1y+zifif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00+yfFgdom1y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
435 319 415 434 syl2anc F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00gdom1y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
436 simplrr fdom1b<1fbvol*f-1ranf00b
437 199 a1i fdom1bvol*f-1ranf00z1fb2vol*f-1ranf0V
438 235 105 ifex ifzf-1ranf010V
439 438 a1i fdom1bvol*f-1ranf00zifzf-1ranf010V
440 fconstmpt ×1fb2vol*f-1ranf0=z1fb2vol*f-1ranf0
441 440 a1i fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0=z1fb2vol*f-1ranf0
442 eqidd fdom1bvol*f-1ranf00zifzf-1ranf010=zifzf-1ranf010
443 196 437 439 441 442 offval2 fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fzifzf-1ranf010=z1fb2vol*f-1ranf0ifzf-1ranf010
444 ovif2 1fb2vol*f-1ranf0ifzf-1ranf010=ifzf-1ranf01fb2vol*f-1ranf011fb2vol*f-1ranf00
445 266 267 ifeq12d fdom1bvol*f-1ranf00ifzf-1ranf01fb2vol*f-1ranf011fb2vol*f-1ranf00=ifzf-1ranf01fb2vol*f-1ranf00
446 444 445 eqtrid fdom1bvol*f-1ranf001fb2vol*f-1ranf0ifzf-1ranf010=ifzf-1ranf01fb2vol*f-1ranf00
447 446 mpteq2dv fdom1bvol*f-1ranf00z1fb2vol*f-1ranf0ifzf-1ranf010=zifzf-1ranf01fb2vol*f-1ranf00
448 443 447 eqtrd fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fzifzf-1ranf010=zifzf-1ranf01fb2vol*f-1ranf00
449 eqid zifzf-1ranf010=zifzf-1ranf010
450 449 i1f1 f-1ranf0domvolvolf-1ranf0zifzf-1ranf010dom1
451 247 252 450 syl2anc fdom1zifzf-1ranf010dom1
452 451 ad2antrr fdom1bvol*f-1ranf00zifzf-1ranf010dom1
453 452 264 i1fmulc fdom1bvol*f-1ranf00×1fb2vol*f-1ranf0×fzifzf-1ranf010dom1
454 448 453 eqeltrrd fdom1bvol*f-1ranf00zifzf-1ranf01fb2vol*f-1ranf00dom1
455 i1fsub fdom1zifzf-1ranf01fb2vol*f-1ranf00dom1ffzifzf-1ranf01fb2vol*f-1ranf00dom1
456 233 454 455 syl2anc fdom1bvol*f-1ranf00ffzifzf-1ranf01fb2vol*f-1ranf00dom1
457 itg1cl ffzifzf-1ranf01fb2vol*f-1ranf00dom11ffzifzf-1ranf01fb2vol*f-1ranf00
458 456 457 syl fdom1bvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf00
459 458 adantlrl fdom1b<1fbvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf00
460 318 adantlrl fdom1b<1fbvol*f-1ranf00zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1
461 itg1cl zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom11zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
462 460 461 syl fdom1b<1fbvol*f-1ranf001zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
463 simplrl fdom1b<1fbvol*f-1ranf00b<1f
464 simpr fdom1bb
465 8 adantr fdom1b1f
466 97 a1i fdom1b2+
467 464 465 466 ltdiv1d fdom1bb<1fb2<1f2
468 recn bb
469 468 2halvesd bb2+b2=b
470 469 oveq1d bb2+b2-b2=bb2
471 468 halfcld bb2
472 471 471 pncand bb2+b2-b2=b2
473 470 472 eqtr3d bbb2=b2
474 473 breq1d bbb2<1f2b2<1f2
475 474 adantl fdom1bbb2<1f2b2<1f2
476 rehalfcl bb2
477 476 adantl fdom1bb2
478 8 rehalfcld fdom11f2
479 478 adantr fdom1b1f2
480 464 477 479 ltsubaddd fdom1bbb2<1f2b<1f2+b2
481 467 475 480 3bitr2d fdom1bb<1fb<1f2+b2
482 481 adantr fdom1bvol*f-1ranf00b<1fb<1f2+b2
483 482 adantlrl fdom1b<1fbvol*f-1ranf00b<1fb<1f2+b2
484 463 483 mpbid fdom1b<1fbvol*f-1ranf00b<1f2+b2
485 452 264 itg1mulc fdom1bvol*f-1ranf001×1fb2vol*f-1ranf0×fzifzf-1ranf010=1fb2vol*f-1ranf01zifzf-1ranf010
486 448 fveq2d fdom1bvol*f-1ranf001×1fb2vol*f-1ranf0×fzifzf-1ranf010=1zifzf-1ranf01fb2vol*f-1ranf00
487 449 itg11 f-1ranf0domvolvolf-1ranf01zifzf-1ranf010=volf-1ranf0
488 247 252 487 syl2anc fdom11zifzf-1ranf010=volf-1ranf0
489 488 oveq2d fdom11fb2vol*f-1ranf01zifzf-1ranf010=1fb2vol*f-1ranf0volf-1ranf0
490 489 ad2antrr fdom1bvol*f-1ranf001fb2vol*f-1ranf01zifzf-1ranf010=1fb2vol*f-1ranf0volf-1ranf0
491 252 recnd fdom1volf-1ranf0
492 491 ad2antrr fdom1bvol*f-1ranf00volf-1ranf0
493 265 492 mulcomd fdom1bvol*f-1ranf001fb2vol*f-1ranf0volf-1ranf0=volf-1ranf01fb2vol*f-1ranf0
494 249 ad2antrr fdom1bvol*f-1ranf00volf-1ranf0=vol*f-1ranf0
495 494 oveq1d fdom1bvol*f-1ranf00volf-1ranf01fb=vol*f-1ranf01fb
496 259 382 mulcomd fdom1bvol*f-1ranf00vol*f-1ranf01fb=1fbvol*f-1ranf0
497 495 496 eqtrd fdom1bvol*f-1ranf00volf-1ranf01fb=1fbvol*f-1ranf0
498 497 oveq1d fdom1bvol*f-1ranf00volf-1ranf01fb2vol*f-1ranf0=1fbvol*f-1ranf02vol*f-1ranf0
499 492 382 384 263 divassd fdom1bvol*f-1ranf00volf-1ranf01fb2vol*f-1ranf0=volf-1ranf01fb2vol*f-1ranf0
500 382 257 259 261 262 divcan5rd fdom1bvol*f-1ranf001fbvol*f-1ranf02vol*f-1ranf0=1fb2
501 498 499 500 3eqtr3d fdom1bvol*f-1ranf00volf-1ranf01fb2vol*f-1ranf0=1fb2
502 490 493 501 3eqtrd fdom1bvol*f-1ranf001fb2vol*f-1ranf01zifzf-1ranf010=1fb2
503 485 486 502 3eqtr3d fdom1bvol*f-1ranf001zifzf-1ranf01fb2vol*f-1ranf00=1fb2
504 503 oveq2d fdom1bvol*f-1ranf001f1zifzf-1ranf01fb2vol*f-1ranf00=1f1fb2
505 itg1sub fdom1zifzf-1ranf01fb2vol*f-1ranf00dom11ffzifzf-1ranf01fb2vol*f-1ranf00=1f1zifzf-1ranf01fb2vol*f-1ranf00
506 233 454 505 syl2anc fdom1bvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf00=1f1zifzf-1ranf01fb2vol*f-1ranf00
507 8 recnd fdom11f
508 507 ad2antrr fdom1bvol*f-1ranf001f
509 468 ad2antlr fdom1bvol*f-1ranf00b
510 508 509 257 261 divsubdird fdom1bvol*f-1ranf001fb2=1f2b2
511 510 oveq2d fdom1bvol*f-1ranf001f1fb2=1f1f2b2
512 507 adantr fdom1b1f
513 512 halfcld fdom1b1f2
514 471 adantl fdom1bb2
515 512 513 514 subsubd fdom1b1f1f2b2=1f-1f2+b2
516 515 adantr fdom1bvol*f-1ranf001f1f2b2=1f-1f2+b2
517 507 2halvesd fdom11f2+1f2=1f
518 517 oveq1d fdom11f2+1f2-1f2=1f1f2
519 507 halfcld fdom11f2
520 519 519 pncand fdom11f2+1f2-1f2=1f2
521 518 520 eqtr3d fdom11f1f2=1f2
522 521 oveq1d fdom11f-1f2+b2=1f2+b2
523 522 ad2antrr fdom1bvol*f-1ranf001f-1f2+b2=1f2+b2
524 511 516 523 3eqtrrd fdom1bvol*f-1ranf001f2+b2=1f1fb2
525 504 506 524 3eqtr4d fdom1bvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf00=1f2+b2
526 525 adantlrl fdom1b<1fbvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf00=1f2+b2
527 484 526 breqtrrd fdom1b<1fbvol*f-1ranf00b<1ffzifzf-1ranf01fb2vol*f-1ranf00
528 456 adantlrl fdom1b<1fbvol*f-1ranf00ffzifzf-1ranf01fb2vol*f-1ranf00dom1
529 id fdom1bvol*f-1ranf00fdom1bvol*f-1ranf00
530 529 adantlrl fdom1b<1fbvol*f-1ranf00fdom1bvol*f-1ranf00
531 233 36 sylan fdom1bvol*f-1ranf00zfz
532 264 adantr fdom1bvol*f-1ranf00z1fb2vol*f-1ranf0
533 531 532 resubcld fdom1bvol*f-1ranf00zfz1fb2vol*f-1ranf0
534 533 leidd fdom1bvol*f-1ranf00zfz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0
535 534 adantr fdom1bvol*f-1ranf00z0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0
536 285 breq2d 0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0
537 536 adantl fdom1bvol*f-1ranf00z0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0
538 535 537 mpbird fdom1bvol*f-1ranf00z0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
539 533 adantr fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0
540 48 a1i fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf00
541 48 a1i fdom1bvol*f-1ranf00z0
542 533 541 ltnled fdom1bvol*f-1ranf00zfz1fb2vol*f-1ranf0<0¬0fz1fb2vol*f-1ranf0
543 542 biimpar fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0<0
544 539 540 543 ltled fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
545 iffalse ¬0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00=0
546 545 breq2d ¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf00
547 546 adantl fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf00
548 544 547 mpbird fdom1bvol*f-1ranf00z¬0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
549 538 548 pm2.61dan fdom1bvol*f-1ranf00zfz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
550 530 549 sylan fdom1b<1fbvol*f-1ranf00zfz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
551 550 adantr fdom1b<1fbvol*f-1ranf00zzf-1ranf0fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
552 iftrue zf-1ranf0ifzf-1ranf01fb2vol*f-1ranf00=1fb2vol*f-1ranf0
553 552 oveq2d zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00=fz1fb2vol*f-1ranf0
554 iba zf-1ranf00fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf0zf-1ranf0
555 554 bicomd zf-1ranf00fz1fb2vol*f-1ranf0zf-1ranf00fz1fb2vol*f-1ranf0
556 555 ifbid zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
557 553 556 breq12d zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
558 557 adantl fdom1b<1fbvol*f-1ranf00zzf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz1fb2vol*f-1ranf0if0fz1fb2vol*f-1ranf0fz1fb2vol*f-1ranf00
559 551 558 mpbird fdom1b<1fbvol*f-1ranf00zzf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
560 35 ad2antrr fdom1b<1fbvol*f-1ranf00f:
561 170 eleq2d f:zf-1ranf0zf-1ranff-10
562 eldif zf-1ranff-10zf-1ranf¬zf-10
563 561 562 bitrdi f:zf-1ranf0zf-1ranf¬zf-10
564 563 notbid f:¬zf-1ranf0¬zf-1ranf¬zf-10
565 564 adantr f:z¬zf-1ranf0¬zf-1ranf¬zf-10
566 pm4.53 ¬zf-1ranf¬zf-10¬zf-1ranfzf-10
567 207 eleq2d f:zf-1ranfz
568 567 biimpar f:zzf-1ranf
569 568 pm2.24d f:z¬zf-1ranffz=0
570 181 simplbda fFnzf-10fz=0
571 570 ex fFnzf-10fz=0
572 180 571 syl f:zf-10fz=0
573 572 adantr f:zzf-10fz=0
574 569 573 jaod f:z¬zf-1ranfzf-10fz=0
575 566 574 biimtrid f:z¬zf-1ranf¬zf-10fz=0
576 565 575 sylbid f:z¬zf-1ranf0fz=0
577 576 imp f:z¬zf-1ranf0fz=0
578 560 577 sylanl1 fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fz=0
579 578 oveq1d fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fz0=00
580 579 224 eqtrdi fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fz0=0
581 580 30 eqbrtrdi fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fz00
582 iffalse ¬zf-1ranf0ifzf-1ranf01fb2vol*f-1ranf00=0
583 582 oveq2d ¬zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00=fz0
584 289 288 sylbir ¬0fz1fb2vol*f-1ranf0¬zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0
585 584 olcs ¬zf-1ranf0if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=0
586 583 585 breq12d ¬zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz00
587 586 adantl fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00fz00
588 581 587 mpbird fdom1b<1fbvol*f-1ranf00z¬zf-1ranf0fzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
589 559 588 pm2.61dan fdom1b<1fbvol*f-1ranf00zfzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
590 589 ralrimiva fdom1b<1fbvol*f-1ranf00zfzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
591 63 a1i fdom1b<1fbvol*f-1ranf00V
592 ovex fzifzf-1ranf01fb2vol*f-1ranf00V
593 592 a1i fdom1b<1fbvol*f-1ranf00zfzifzf-1ranf01fb2vol*f-1ranf00V
594 422 a1i fdom1b<1fbvol*f-1ranf00zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00V
595 fvex fzV
596 595 a1i fdom1b<1fbvol*f-1ranf00zfzV
597 199 105 ifex ifzf-1ranf01fb2vol*f-1ranf00V
598 597 a1i fdom1b<1fbvol*f-1ranf00zifzf-1ranf01fb2vol*f-1ranf00V
599 70 ad2antrr fdom1b<1fbvol*f-1ranf00f=zfz
600 eqidd fdom1b<1fbvol*f-1ranf00zifzf-1ranf01fb2vol*f-1ranf00=zifzf-1ranf01fb2vol*f-1ranf00
601 591 596 598 599 600 offval2 fdom1b<1fbvol*f-1ranf00ffzifzf-1ranf01fb2vol*f-1ranf00=zfzifzf-1ranf01fb2vol*f-1ranf00
602 eqidd fdom1b<1fbvol*f-1ranf00zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
603 591 593 594 601 602 ofrfval2 fdom1b<1fbvol*f-1ranf00ffzifzf-1ranf01fb2vol*f-1ranf00fzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00zfzifzf-1ranf01fb2vol*f-1ranf00if0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
604 590 603 mpbird fdom1b<1fbvol*f-1ranf00ffzifzf-1ranf01fb2vol*f-1ranf00fzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
605 itg1le ffzifzf-1ranf01fb2vol*f-1ranf00dom1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00dom1ffzifzf-1ranf01fb2vol*f-1ranf00fzif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf001zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
606 528 460 604 605 syl3anc fdom1b<1fbvol*f-1ranf001ffzifzf-1ranf01fb2vol*f-1ranf001zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
607 436 459 462 527 606 ltletrd fdom1b<1fbvol*f-1ranf00b<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
608 607 adantllr fdom1ffFs=1fb<1fbvol*f-1ranf00b<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
609 608 adantlll F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00b<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
610 fvex 1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00V
611 eqeq1 a=1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00a=1g1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
612 611 anbi2d a=1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00y+zifgz=00gz+yfFa=1gy+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
613 612 rexbidv a=1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00gdom1y+zifgz=00gz+yfFa=1ggdom1y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1g
614 breq2 a=1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00b<ab<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
615 613 614 anbi12d a=1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00gdom1y+zifgz=00gz+yfFa=1gb<agdom1y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1gb<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00
616 610 615 spcev gdom1y+zifgz=00gz+yfF1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00=1gb<1zif0fz1fb2vol*f-1ranf0zf-1ranf0fz1fb2vol*f-1ranf00agdom1y+zifgz=00gz+yfFa=1gb<a
617 435 609 616 syl2anc F:0+∞fdom1ffFs=1fb<1fbvol*f-1ranf00agdom1y+zifgz=00gz+yfFa=1gb<a
618 192 617 pm2.61dane F:0+∞fdom1ffFs=1fb<1fbagdom1y+zifgz=00gz+yfFa=1gb<a
619 618 expr F:0+∞fdom1ffFs=1fb<1fbagdom1y+zifgz=00gz+yfFa=1gb<a
620 619 adantllr F:0+∞b*fdom1ffFs=1fb<1fbagdom1y+zifgz=00gz+yfFa=1gb<a
621 620 adantr F:0+∞b*fdom1ffFs=1fb<1fb−∞bagdom1y+zifgz=00gz+yfFa=1gb<a
622 157 621 mpd F:0+∞b*fdom1ffFs=1fb<1fb−∞agdom1y+zifgz=00gz+yfFa=1gb<a
623 139 622 pm2.61dane F:0+∞b*fdom1ffFs=1fb<1fagdom1y+zifgz=00gz+yfFa=1gb<a
624 623 ex F:0+∞b*fdom1ffFs=1fb<1fagdom1y+zifgz=00gz+yfFa=1gb<a
625 94 624 sylbid F:0+∞b*fdom1ffFs=1fb<sagdom1y+zifgz=00gz+yfFa=1gb<a
626 625 imp F:0+∞b*fdom1ffFs=1fb<sagdom1y+zifgz=00gz+yfFa=1gb<a
627 626 an32s F:0+∞b*b<sfdom1ffFs=1fagdom1y+zifgz=00gz+yfFa=1gb<a
628 627 rexlimdvaa F:0+∞b*b<sfdom1ffFs=1fagdom1y+zifgz=00gz+yfFa=1gb<a
629 628 expimpd F:0+∞b*b<sfdom1ffFs=1fagdom1y+zifgz=00gz+yfFa=1gb<a
630 629 ancomsd F:0+∞b*fdom1ffFs=1fb<sagdom1y+zifgz=00gz+yfFa=1gb<a
631 630 exlimdv F:0+∞b*sfdom1ffFs=1fb<sagdom1y+zifgz=00gz+yfFa=1gb<a
632 eqeq1 x=sx=1fs=1f
633 632 anbi2d x=sffFx=1fffFs=1f
634 633 rexbidv x=sfdom1ffFx=1ffdom1ffFs=1f
635 634 rexab sx|fdom1ffFx=1fb<ssfdom1ffFs=1fb<s
636 eqeq1 x=ax=1ga=1g
637 636 anbi2d x=ay+zifgz=00gz+yfFx=1gy+zifgz=00gz+yfFa=1g
638 637 rexbidv x=agdom1y+zifgz=00gz+yfFx=1ggdom1y+zifgz=00gz+yfFa=1g
639 638 rexab ax|gdom1y+zifgz=00gz+yfFx=1gb<aagdom1y+zifgz=00gz+yfFa=1gb<a
640 631 635 639 3imtr4g F:0+∞b*sx|fdom1ffFx=1fb<sax|gdom1y+zifgz=00gz+yfFx=1gb<a
641 92 640 sylbid F:0+∞b*b<supx|fdom1ffFx=1f*<ax|gdom1y+zifgz=00gz+yfFx=1gb<a
642 641 impr F:0+∞b*b<supx|fdom1ffFx=1f*<ax|gdom1y+zifgz=00gz+yfFx=1gb<a
643 6 15 89 642 eqsupd F:0+∞supx|gdom1y+zifgz=00gz+yfFx=1g*<=supx|fdom1ffFx=1f*<
644 4 643 eqtrid F:0+∞supL*<=supx|fdom1ffFx=1f*<
645 3 644 eqtr4d F:0+∞2F=supL*<