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 | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g
Assertion itg2addnclem F : 0 +∞ 2 F = sup L * <

Proof

Step Hyp Ref Expression
1 itg2addnclem.1 L = x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g
2 eqid x | f dom 1 f f F x = 1 f = x | f dom 1 f f F x = 1 f
3 2 itg2val F : 0 +∞ 2 F = sup x | f dom 1 f f F x = 1 f * <
4 1 supeq1i sup L * < = sup x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g * <
5 xrltso < Or *
6 5 a1i F : 0 +∞ < Or *
7 simprr f dom 1 f f F x = 1 f x = 1 f
8 itg1cl f dom 1 1 f
9 8 rexrd f dom 1 1 f *
10 9 adantr f dom 1 f f F x = 1 f 1 f *
11 7 10 eqeltrd f dom 1 f f F x = 1 f x *
12 11 rexlimiva f dom 1 f f F x = 1 f x *
13 12 abssi x | f dom 1 f f F x = 1 f *
14 supxrcl x | f dom 1 f f F x = 1 f * sup x | f dom 1 f f F x = 1 f * < *
15 13 14 mp1i F : 0 +∞ sup x | f dom 1 f f F x = 1 f * < *
16 fveq1 g = f g z = f z
17 16 eqeq1d g = f g z = 0 f z = 0
18 16 oveq1d g = f g z + y = f z + y
19 17 18 ifbieq2d g = f if g z = 0 0 g z + y = if f z = 0 0 f z + y
20 19 mpteq2dv g = f z if g z = 0 0 g z + y = z if f z = 0 0 f z + y
21 20 breq1d g = f z if g z = 0 0 g z + y f F z if f z = 0 0 f z + y f F
22 21 rexbidv g = f y + z if g z = 0 0 g z + y f F y + z if f z = 0 0 f z + y f F
23 fveq2 g = f 1 g = 1 f
24 23 eqeq2d g = f x = 1 g x = 1 f
25 22 24 anbi12d g = f y + z if g z = 0 0 g z + y f F x = 1 g y + z if f z = 0 0 f z + y f F x = 1 f
26 25 cbvrexvw g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g f dom 1 y + z if f z = 0 0 f z + y f F x = 1 f
27 breq2 0 = if f z = 0 0 f z + y f z 0 f z if f z = 0 0 f z + y
28 breq2 f z + y = if f z = 0 0 f z + y f z f z + y f z if f z = 0 0 f z + y
29 id f z = 0 f z = 0
30 0le0 0 0
31 29 30 eqbrtrdi f z = 0 f z 0
32 31 adantl f dom 1 y + z f z = 0 f z 0
33 rpge0 y + 0 y
34 33 ad2antlr f dom 1 y + z 0 y
35 i1ff f dom 1 f :
36 35 ffvelrnda f dom 1 z f z
37 36 adantlr f dom 1 y + z f z
38 rpre y + y
39 38 ad2antlr f dom 1 y + z y
40 37 39 addge01d f dom 1 y + z 0 y f z f z + y
41 34 40 mpbid f dom 1 y + z f z f z + y
42 41 adantr f dom 1 y + z ¬ f z = 0 f z f z + y
43 27 28 32 42 ifbothda f dom 1 y + z f z if f z = 0 0 f z + y
44 43 adantlll F : 0 +∞ f dom 1 y + z f z if f z = 0 0 f z + y
45 35 ad2antlr F : 0 +∞ f dom 1 y + f :
46 45 ffvelrnda F : 0 +∞ f dom 1 y + z f z
47 46 rexrd F : 0 +∞ f dom 1 y + z f z *
48 0re 0
49 38 ad2antlr F : 0 +∞ f dom 1 y + z y
50 46 49 readdcld F : 0 +∞ f dom 1 y + z f z + y
51 ifcl 0 f z + y if f z = 0 0 f z + y
52 48 50 51 sylancr F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y
53 52 rexrd F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y *
54 iccssxr 0 +∞ *
55 fss F : 0 +∞ 0 +∞ * F : *
56 54 55 mpan2 F : 0 +∞ F : *
57 56 ad2antrr F : 0 +∞ f dom 1 y + F : *
58 57 ffvelrnda F : 0 +∞ f dom 1 y + z F z *
59 xrletr f z * if f z = 0 0 f z + y * F z * f z if f z = 0 0 f z + y if f z = 0 0 f z + y F z f z F z
60 47 53 58 59 syl3anc F : 0 +∞ f dom 1 y + z f z if f z = 0 0 f z + y if f z = 0 0 f z + y F z f z F z
61 44 60 mpand F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y F z f z F z
62 61 ralimdva F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y F z z f z F z
63 reex V
64 63 a1i F : 0 +∞ f dom 1 y + V
65 eqidd F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y = z if f z = 0 0 f z + y
66 id F : 0 +∞ F : 0 +∞
67 66 feqmptd F : 0 +∞ F = z F z
68 67 ad2antrr F : 0 +∞ f dom 1 y + F = z F z
69 64 52 58 65 68 ofrfval2 F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y f F z if f z = 0 0 f z + y F z
70 35 feqmptd f dom 1 f = z f z
71 70 ad2antlr F : 0 +∞ f dom 1 y + f = z f z
72 64 46 58 71 68 ofrfval2 F : 0 +∞ f dom 1 y + f f F z f z F z
73 62 69 72 3imtr4d F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y f F f f F
74 73 rexlimdva F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y f F f f F
75 74 anim1d F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y f F x = 1 f f f F x = 1 f
76 75 reximdva F : 0 +∞ f dom 1 y + z if f z = 0 0 f z + y f F x = 1 f f dom 1 f f F x = 1 f
77 26 76 syl5bi F : 0 +∞ g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g f dom 1 f f F x = 1 f
78 77 ss2abdv F : 0 +∞ x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g x | f dom 1 f f F x = 1 f
79 78 sseld F : 0 +∞ b x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g b x | f dom 1 f f F x = 1 f
80 simp3r F : 0 +∞ f dom 1 f f F x = 1 f x = 1 f
81 9 3ad2ant2 F : 0 +∞ f dom 1 f f F x = 1 f 1 f *
82 80 81 eqeltrd F : 0 +∞ f dom 1 f f F x = 1 f x *
83 82 rexlimdv3a F : 0 +∞ f dom 1 f f F x = 1 f x *
84 83 abssdv F : 0 +∞ x | f dom 1 f f F x = 1 f *
85 xrsupss x | f dom 1 f f F x = 1 f * a * b x | f dom 1 f f F x = 1 f ¬ a < b b * b < a s x | f dom 1 f f F x = 1 f b < s
86 84 85 syl F : 0 +∞ a * b x | f dom 1 f f F x = 1 f ¬ a < b b * b < a s x | f dom 1 f f F x = 1 f b < s
87 6 86 supub F : 0 +∞ b x | f dom 1 f f F x = 1 f ¬ sup x | f dom 1 f f F x = 1 f * < < b
88 79 87 syld F : 0 +∞ b x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g ¬ sup x | f dom 1 f f F x = 1 f * < < b
89 88 imp F : 0 +∞ b x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g ¬ sup x | f dom 1 f f F x = 1 f * < < b
90 supxrlub x | f dom 1 f f F x = 1 f * b * b < sup x | f dom 1 f f F x = 1 f * < s x | f dom 1 f f F x = 1 f b < s
91 13 90 mpan b * b < sup x | f dom 1 f f F x = 1 f * < s x | f dom 1 f f F x = 1 f b < s
92 91 adantl F : 0 +∞ b * b < sup x | f dom 1 f f F x = 1 f * < s x | f dom 1 f f F x = 1 f b < s
93 simprrr F : 0 +∞ b * f dom 1 f f F s = 1 f s = 1 f
94 93 breq2d F : 0 +∞ b * f dom 1 f f F s = 1 f b < s b < 1 f
95 simplll F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f F : 0 +∞
96 i1f0 × 0 dom 1
97 2rp 2 +
98 97 ne0ii +
99 ffvelrn F : 0 +∞ z F z 0 +∞
100 elxrge0 F z 0 +∞ F z * 0 F z
101 99 100 sylib F : 0 +∞ z F z * 0 F z
102 101 simprd F : 0 +∞ z 0 F z
103 102 ralrimiva F : 0 +∞ z 0 F z
104 63 a1i F : 0 +∞ V
105 c0ex 0 V
106 105 a1i F : 0 +∞ z 0 V
107 eqidd F : 0 +∞ z 0 = z 0
108 104 106 99 107 67 ofrfval2 F : 0 +∞ z 0 f F z 0 F z
109 103 108 mpbird F : 0 +∞ z 0 f F
110 109 ralrimivw F : 0 +∞ y + z 0 f F
111 r19.2z + y + z 0 f F y + z 0 f F
112 98 110 111 sylancr F : 0 +∞ y + z 0 f F
113 fveq2 g = × 0 1 g = 1 × 0
114 itg10 1 × 0 = 0
115 113 114 eqtr2di g = × 0 0 = 1 g
116 115 biantrud g = × 0 y + z if g z = 0 0 g z + y f F y + z if g z = 0 0 g z + y f F 0 = 1 g
117 fveq1 g = × 0 g z = × 0 z
118 105 fvconst2 z × 0 z = 0
119 117 118 sylan9eq g = × 0 z g z = 0
120 iftrue g z = 0 if g z = 0 0 g z + y = 0
121 119 120 syl g = × 0 z if g z = 0 0 g z + y = 0
122 121 mpteq2dva g = × 0 z if g z = 0 0 g z + y = z 0
123 122 breq1d g = × 0 z if g z = 0 0 g z + y f F z 0 f F
124 123 rexbidv g = × 0 y + z if g z = 0 0 g z + y f F y + z 0 f F
125 116 124 bitr3d g = × 0 y + z if g z = 0 0 g z + y f F 0 = 1 g y + z 0 f F
126 125 rspcev × 0 dom 1 y + z 0 f F g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g
127 96 112 126 sylancr F : 0 +∞ g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g
128 id b = −∞ b = −∞
129 mnflt 0 −∞ < 0
130 48 129 mp1i b = −∞ −∞ < 0
131 128 130 eqbrtrd b = −∞ b < 0
132 eqeq1 a = 0 a = 1 g 0 = 1 g
133 132 anbi2d a = 0 y + z if g z = 0 0 g z + y f F a = 1 g y + z if g z = 0 0 g z + y f F 0 = 1 g
134 133 rexbidv a = 0 g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g
135 breq2 a = 0 b < a b < 0
136 134 135 anbi12d a = 0 g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g b < 0
137 105 136 spcev g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g b < 0 a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
138 127 131 137 syl2an F : 0 +∞ b = −∞ a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
139 95 138 sylan F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b = −∞ a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
140 simp-4r F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ b *
141 8 adantr f dom 1 f f F s = 1 f 1 f
142 141 ad3antlr F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ 1 f
143 simpllr F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b *
144 ngtmnft b * b = −∞ ¬ −∞ < b
145 144 biimprd b * ¬ −∞ < b b = −∞
146 145 necon1ad b * b −∞ −∞ < b
147 146 imp b * b −∞ −∞ < b
148 143 147 sylan F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ −∞ < b
149 simpr F : 0 +∞ b * b *
150 9 adantr f dom 1 f f F s = 1 f 1 f *
151 149 150 anim12i F : 0 +∞ b * f dom 1 f f F s = 1 f b * 1 f *
152 xrltle b * 1 f * b < 1 f b 1 f
153 152 imp b * 1 f * b < 1 f b 1 f
154 151 153 sylan F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b 1 f
155 154 adantr F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ b 1 f
156 xrre b * 1 f −∞ < b b 1 f b
157 140 142 148 155 156 syl22anc F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ b
158 127 ad3antrrr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 = 0 g dom 1 y + z if g z = 0 0 g z + y f F 0 = 1 g
159 simplrl F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 = 0 b < 1 f
160 simplrl F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b f dom 1
161 simpl f dom 1 vol * f -1 ran f 0 = 0 f dom 1
162 cnvimass f -1 ran f 0 dom f
163 162 35 fssdm f dom 1 f -1 ran f 0
164 163 adantr f dom 1 vol * f -1 ran f 0 = 0 f -1 ran f 0
165 simpr f dom 1 vol * f -1 ran f 0 = 0 vol * f -1 ran f 0 = 0
166 fdm f : dom f =
167 166 eqcomd f : = dom f
168 ffun f : Fun f
169 difpreima Fun f f -1 ran f 0 = f -1 ran f f -1 0
170 168 169 syl f : f -1 ran f 0 = f -1 ran f f -1 0
171 cnvimarndm f -1 ran f = dom f
172 171 difeq1i f -1 ran f f -1 0 = dom f f -1 0
173 170 172 eqtrdi f : f -1 ran f 0 = dom f f -1 0
174 167 173 difeq12d f : f -1 ran f 0 = dom f dom f f -1 0
175 cnvimass f -1 0 dom f
176 dfss4 f -1 0 dom f dom f dom f f -1 0 = f -1 0
177 175 176 mpbi dom f dom f f -1 0 = f -1 0
178 174 177 eqtrdi f : f -1 ran f 0 = f -1 0
179 178 eleq2d f : z f -1 ran f 0 z f -1 0
180 ffn f : f Fn
181 fniniseg f Fn z f -1 0 z f z = 0
182 simpr z f z = 0 f z = 0
183 181 182 syl6bi f Fn z f -1 0 f z = 0
184 180 183 syl f : z f -1 0 f z = 0
185 179 184 sylbid f : z f -1 ran f 0 f z = 0
186 35 185 syl f dom 1 z f -1 ran f 0 f z = 0
187 186 imp f dom 1 z f -1 ran f 0 f z = 0
188 187 adantlr f dom 1 vol * f -1 ran f 0 = 0 z f -1 ran f 0 f z = 0
189 161 164 165 188 itg10a f dom 1 vol * f -1 ran f 0 = 0 1 f = 0
190 160 189 sylan F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 = 0 1 f = 0
191 159 190 breqtrd F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 = 0 b < 0
192 158 191 137 syl2anc F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 = 0 a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
193 simprl F : 0 +∞ f dom 1 f f F s = 1 f f dom 1
194 simpr b < 1 f b b
195 193 194 anim12i F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b f dom 1 b
196 63 a1i f dom 1 b vol * f -1 ran f 0 0 V
197 fvex f u V
198 197 a1i f dom 1 b vol * f -1 ran f 0 0 u f u V
199 ovex 1 f b 2 vol * f -1 ran f 0 V
200 199 105 ifex if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
201 200 a1i f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
202 35 feqmptd f dom 1 f = u f u
203 202 ad2antrr f dom 1 b vol * f -1 ran f 0 0 f = u f u
204 eqidd f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
205 196 198 201 203 204 offval2 f dom 1 b vol * f -1 ran f 0 0 f f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = u f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
206 ovif2 f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 f u 0
207 171 166 syl5eq f : f -1 ran f =
208 207 difeq1d f : f -1 ran f f -1 0 = f -1 0
209 170 208 eqtrd f : f -1 ran f 0 = f -1 0
210 209 eleq2d f : u f -1 ran f 0 u f -1 0
211 35 210 syl f dom 1 u f -1 ran f 0 u f -1 0
212 211 ad3antrrr f dom 1 b vol * f -1 ran f 0 0 u u f -1 ran f 0 u f -1 0
213 simpr f dom 1 b vol * f -1 ran f 0 0 u u
214 213 biantrurd f dom 1 b vol * f -1 ran f 0 0 u ¬ u f -1 0 u ¬ u f -1 0
215 eldif u f -1 0 u ¬ u f -1 0
216 214 215 bitr4di f dom 1 b vol * f -1 ran f 0 0 u ¬ u f -1 0 u f -1 0
217 212 216 bitr4d f dom 1 b vol * f -1 ran f 0 0 u u f -1 ran f 0 ¬ u f -1 0
218 217 con2bid f dom 1 b vol * f -1 ran f 0 0 u u f -1 0 ¬ u f -1 ran f 0
219 fniniseg f Fn u f -1 0 u f u = 0
220 35 180 219 3syl f dom 1 u f -1 0 u f u = 0
221 220 ad3antrrr f dom 1 b vol * f -1 ran f 0 0 u u f -1 0 u f u = 0
222 218 221 bitr3d f dom 1 b vol * f -1 ran f 0 0 u ¬ u f -1 ran f 0 u f u = 0
223 oveq1 f u = 0 f u 0 = 0 0
224 0m0e0 0 0 = 0
225 223 224 eqtrdi f u = 0 f u 0 = 0
226 225 adantl u f u = 0 f u 0 = 0
227 222 226 syl6bi f dom 1 b vol * f -1 ran f 0 0 u ¬ u f -1 ran f 0 f u 0 = 0
228 227 imp f dom 1 b vol * f -1 ran f 0 0 u ¬ u f -1 ran f 0 f u 0 = 0
229 228 ifeq2da f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 f u 0 = if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0
230 206 229 syl5eq f dom 1 b vol * f -1 ran f 0 0 u f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0
231 230 mpteq2dva f dom 1 b vol * f -1 ran f 0 0 u f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0
232 205 231 eqtrd f dom 1 b vol * f -1 ran f 0 0 f f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0
233 simpll f dom 1 b vol * f -1 ran f 0 0 f dom 1
234 199 a1i f dom 1 b vol * f -1 ran f 0 0 u 1 f b 2 vol * f -1 ran f 0 V
235 1ex 1 V
236 235 105 ifex if u f -1 ran f 0 1 0 V
237 236 a1i f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 0 V
238 fconstmpt × 1 f b 2 vol * f -1 ran f 0 = u 1 f b 2 vol * f -1 ran f 0
239 238 a1i f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 = u 1 f b 2 vol * f -1 ran f 0
240 eqidd f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 0 = u if u f -1 ran f 0 1 0
241 196 234 237 239 240 offval2 f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f u if u f -1 ran f 0 1 0 = u 1 f b 2 vol * f -1 ran f 0 if u f -1 ran f 0 1 0
242 ovif2 1 f b 2 vol * f -1 ran f 0 if u f -1 ran f 0 1 0 = if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 1 1 f b 2 vol * f -1 ran f 0 0
243 resubcl 1 f b 1 f b
244 8 243 sylan f dom 1 b 1 f b
245 244 adantr f dom 1 b vol * f -1 ran f 0 0 1 f b
246 2re 2
247 i1fima f dom 1 f -1 ran f 0 dom vol
248 mblvol f -1 ran f 0 dom vol vol f -1 ran f 0 = vol * f -1 ran f 0
249 247 248 syl f dom 1 vol f -1 ran f 0 = vol * f -1 ran f 0
250 neldifsn ¬ 0 ran f 0
251 i1fima2 f dom 1 ¬ 0 ran f 0 vol f -1 ran f 0
252 250 251 mpan2 f dom 1 vol f -1 ran f 0
253 249 252 eqeltrrd f dom 1 vol * f -1 ran f 0
254 remulcl 2 vol * f -1 ran f 0 2 vol * f -1 ran f 0
255 246 253 254 sylancr f dom 1 2 vol * f -1 ran f 0
256 255 ad2antrr f dom 1 b vol * f -1 ran f 0 0 2 vol * f -1 ran f 0
257 2cnd f dom 1 b vol * f -1 ran f 0 0 2
258 253 ad2antrr f dom 1 b vol * f -1 ran f 0 0 vol * f -1 ran f 0
259 258 recnd f dom 1 b vol * f -1 ran f 0 0 vol * f -1 ran f 0
260 2ne0 2 0
261 260 a1i f dom 1 b vol * f -1 ran f 0 0 2 0
262 simpr f dom 1 b vol * f -1 ran f 0 0 vol * f -1 ran f 0 0
263 257 259 261 262 mulne0d f dom 1 b vol * f -1 ran f 0 0 2 vol * f -1 ran f 0 0
264 245 256 263 redivcld f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0
265 264 recnd f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0
266 265 mulid1d f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 1 = 1 f b 2 vol * f -1 ran f 0
267 265 mul01d f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 0 = 0
268 266 267 ifeq12d f dom 1 b vol * f -1 ran f 0 0 if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 1 1 f b 2 vol * f -1 ran f 0 0 = if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
269 242 268 syl5eq f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 if u f -1 ran f 0 1 0 = if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
270 269 mpteq2dv f dom 1 b vol * f -1 ran f 0 0 u 1 f b 2 vol * f -1 ran f 0 if u f -1 ran f 0 1 0 = u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
271 241 270 eqtrd f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f u if u f -1 ran f 0 1 0 = u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
272 eqid u if u f -1 ran f 0 1 0 = u if u f -1 ran f 0 1 0
273 272 i1f1 f -1 ran f 0 dom vol vol f -1 ran f 0 u if u f -1 ran f 0 1 0 dom 1
274 247 252 273 syl2anc f dom 1 u if u f -1 ran f 0 1 0 dom 1
275 274 ad2antrr f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 0 dom 1
276 275 264 i1fmulc f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f u if u f -1 ran f 0 1 0 dom 1
277 271 276 eqeltrrd f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
278 i1fsub f dom 1 u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1 f f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
279 233 277 278 syl2anc f dom 1 b vol * f -1 ran f 0 0 f f u if u f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
280 232 279 eqeltrrd f dom 1 b vol * f -1 ran f 0 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 dom 1
281 iftrue 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = f z 1 f b 2 vol * f -1 ran f 0
282 iftrue z f -1 ran f 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = f z 1 f b 2 vol * f -1 ran f 0
283 282 breq2d z f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 f z 1 f b 2 vol * f -1 ran f 0
284 283 282 ifbieq1d z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
285 iftrue 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = f z 1 f b 2 vol * f -1 ran f 0
286 284 285 sylan9eqr 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = f z 1 f b 2 vol * f -1 ran f 0
287 281 286 eqtr4d 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0
288 iffalse ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
289 ianor ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 ¬ z f -1 ran f 0
290 283 ifbid z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0
291 iffalse ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
292 290 291 sylan9eqr ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
293 292 ex ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
294 iffalse ¬ z f -1 ran f 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
295 eqid 0 = 0
296 eqeq1 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
297 eqeq1 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 0 = 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
298 296 297 ifboth if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 = 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
299 294 295 298 sylancl ¬ z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
300 293 299 pm2.61d1 ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
301 300 299 jaoi ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 ¬ z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
302 289 301 sylbi ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 = 0
303 288 302 eqtr4d ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0
304 287 303 pm2.61i if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0
305 eleq1w u = z u f -1 ran f 0 z f -1 ran f 0
306 fveq2 u = z f u = f z
307 306 oveq1d u = z f u 1 f b 2 vol * f -1 ran f 0 = f z 1 f b 2 vol * f -1 ran f 0
308 305 307 ifbieq1d u = z if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 = if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
309 eqid u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 = u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0
310 ovex f z 1 f b 2 vol * f -1 ran f 0 V
311 310 105 ifex if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 V
312 308 309 311 fvmpt z u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z = if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
313 312 breq2d z 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
314 313 312 ifbieq1d z if 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z 0 = if 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 if z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0
315 304 314 eqtr4id z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z 0
316 315 mpteq2ia z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = z if 0 u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 z 0
317 316 i1fpos u if u f -1 ran f 0 f u 1 f b 2 vol * f -1 ran f 0 0 dom 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1
318 280 317 syl f dom 1 b vol * f -1 ran f 0 0 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1
319 195 318 sylan F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1
320 195 264 sylan F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0
321 8 ad2antrl F : 0 +∞ f dom 1 f f F s = 1 f 1 f
322 321 194 243 syl2an F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b 1 f b
323 322 adantr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 1 f b
324 255 adantr f dom 1 f f F s = 1 f 2 vol * f -1 ran f 0
325 324 ad3antlr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 2 vol * f -1 ran f 0
326 simprl F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b b < 1 f
327 simprr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b b
328 141 ad2antlr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b 1 f
329 327 328 posdifd F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b b < 1 f 0 < 1 f b
330 326 329 mpbid F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b 0 < 1 f b
331 330 adantr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 0 < 1 f b
332 253 adantr f dom 1 f f F s = 1 f vol * f -1 ran f 0
333 332 ad3antlr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 vol * f -1 ran f 0
334 mblss f -1 ran f 0 dom vol f -1 ran f 0
335 ovolge0 f -1 ran f 0 0 vol * f -1 ran f 0
336 247 334 335 3syl f dom 1 0 vol * f -1 ran f 0
337 ltlen 0 vol * f -1 ran f 0 0 < vol * f -1 ran f 0 0 vol * f -1 ran f 0 vol * f -1 ran f 0 0
338 48 253 337 sylancr f dom 1 0 < vol * f -1 ran f 0 0 vol * f -1 ran f 0 vol * f -1 ran f 0 0
339 338 biimprd f dom 1 0 vol * f -1 ran f 0 vol * f -1 ran f 0 0 0 < vol * f -1 ran f 0
340 336 339 mpand f dom 1 vol * f -1 ran f 0 0 0 < vol * f -1 ran f 0
341 340 ad2antrl F : 0 +∞ f dom 1 f f F s = 1 f vol * f -1 ran f 0 0 0 < vol * f -1 ran f 0
342 341 imp F : 0 +∞ f dom 1 f f F s = 1 f vol * f -1 ran f 0 0 0 < vol * f -1 ran f 0
343 342 adantlr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 0 < vol * f -1 ran f 0
344 2pos 0 < 2
345 mulgt0 2 0 < 2 vol * f -1 ran f 0 0 < vol * f -1 ran f 0 0 < 2 vol * f -1 ran f 0
346 246 344 345 mpanl12 vol * f -1 ran f 0 0 < vol * f -1 ran f 0 0 < 2 vol * f -1 ran f 0
347 333 343 346 syl2anc F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 0 < 2 vol * f -1 ran f 0
348 323 325 331 347 divgt0d F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 0 < 1 f b 2 vol * f -1 ran f 0
349 320 348 elrpd F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 +
350 simprl f dom 1 f f F s = 1 f f f F
351 350 ad3antlr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 f f F
352 ffn F : 0 +∞ F Fn
353 35 180 syl f dom 1 f Fn
354 353 adantr f dom 1 f f F s = 1 f f Fn
355 simpr F Fn f Fn f Fn
356 simpl F Fn f Fn F Fn
357 63 a1i F Fn f Fn V
358 inidm =
359 eqidd F Fn f Fn z f z = f z
360 eqidd F Fn f Fn z F z = F z
361 355 356 357 357 358 359 360 ofrfval F Fn f Fn f f F z f z F z
362 352 354 361 syl2an F : 0 +∞ f dom 1 f f F s = 1 f f f F z f z F z
363 362 ad2antrr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 f f F z f z F z
364 simpl f dom 1 f f F s = 1 f f dom 1
365 364 anim2i F : 0 +∞ f dom 1 f f F s = 1 f F : 0 +∞ f dom 1
366 365 194 anim12i F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b F : 0 +∞ f dom 1 b
367 breq1 0 = if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 0 F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
368 breq1 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 = if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
369 simplll F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 F : 0 +∞
370 369 ffvelrnda F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z F z 0 +∞
371 370 100 sylib F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z F z * 0 F z
372 371 simprd F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z 0 F z
373 372 ad2antrr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 F z
374 oveq1 f z 1 f b 2 vol * f -1 ran f 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
375 374 breq1d f z 1 f b 2 vol * f -1 ran f 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 F z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
376 oveq1 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 + 1 f b 2 vol * f -1 ran f 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
377 376 breq1d 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 0 + 1 f b 2 vol * f -1 ran f 0 F z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
378 35 ad3antlr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 f :
379 378 ffvelrnda F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z
380 379 recnd F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z
381 244 recnd f dom 1 b 1 f b
382 381 adantr f dom 1 b vol * f -1 ran f 0 0 1 f b
383 255 recnd f dom 1 2 vol * f -1 ran f 0
384 383 ad2antrr f dom 1 b vol * f -1 ran f 0 0 2 vol * f -1 ran f 0
385 382 384 263 divcld f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0
386 385 adantlll F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0
387 386 adantr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z 1 f b 2 vol * f -1 ran f 0
388 380 387 npcand F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 = f z
389 388 adantr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 = f z
390 simpr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z f z F z
391 389 390 eqbrtrd F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 F z
392 391 ad2antrr F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z ¬ if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z - 1 f b 2 vol * f -1 ran f 0 + 1 f b 2 vol * f -1 ran f 0 F z
393 288 pm2.24d ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 ¬ if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
394 393 impcom ¬ if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
395 394 adantll F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z ¬ if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
396 375 377 392 395 ifbothda F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z ¬ if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
397 367 368 373 396 ifbothda F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
398 397 ex F : 0 +∞ f dom 1 b vol * f -1 ran f 0 0 z f z F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
399 366 398 sylanl1 F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z f z F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
400 399 ralimdva F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z f z F z z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
401 363 400 sylbid F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 f f F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
402 351 401 mpd F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
403 ovex if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 V
404 105 403 ifex if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 V
405 404 a1i F : 0 +∞ z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 V
406 eqidd F : 0 +∞ z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 = z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
407 104 405 99 406 67 ofrfval2 F : 0 +∞ z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 f F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
408 407 ad3antrrr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 f F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 F z
409 402 408 mpbird F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 f F
410 oveq2 y = 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
411 410 ifeq2d y = 1 f b 2 vol * f -1 ran f 0 if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y = if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
412 411 mpteq2dv y = 1 f b 2 vol * f -1 ran f 0 z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y = z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0
413 412 breq1d y = 1 f b 2 vol * f -1 ran f 0 z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 f F
414 413 rspcev 1 f b 2 vol * f -1 ran f 0 + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + 1 f b 2 vol * f -1 ran f 0 f F y + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F
415 349 409 414 syl2anc F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 y + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F
416 fveq2 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = g 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
417 416 eqcoms g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
418 417 biantrud g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 y + z if g z = 0 0 g z + y f F y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
419 nfmpt1 _ z z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
420 419 nfeq2 z g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
421 fveq1 g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 g z = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z
422 310 105 ifex if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 V
423 eqid z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
424 423 fvmpt2 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 V z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
425 422 424 mpan2 z z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
426 421 425 sylan9eq g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z g z = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
427 426 eqeq1d g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z g z = 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
428 426 oveq1d g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z g z + y = if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y
429 427 428 ifbieq2d g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z if g z = 0 0 g z + y = if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y
430 420 429 mpteq2da g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z if g z = 0 0 g z + y = z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y
431 430 breq1d g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z if g z = 0 0 g z + y f F z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F
432 431 rexbidv g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 y + z if g z = 0 0 g z + y f F y + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F
433 418 432 bitr3d g = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g y + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F
434 433 rspcev z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1 y + z if if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 + y f F g dom 1 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
435 319 415 434 syl2anc F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 g dom 1 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
436 simplrr f dom 1 b < 1 f b vol * f -1 ran f 0 0 b
437 199 a1i f dom 1 b vol * f -1 ran f 0 0 z 1 f b 2 vol * f -1 ran f 0 V
438 235 105 ifex if z f -1 ran f 0 1 0 V
439 438 a1i f dom 1 b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 0 V
440 fconstmpt × 1 f b 2 vol * f -1 ran f 0 = z 1 f b 2 vol * f -1 ran f 0
441 440 a1i f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 = z 1 f b 2 vol * f -1 ran f 0
442 eqidd f dom 1 b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 0 = z if z f -1 ran f 0 1 0
443 196 437 439 441 442 offval2 f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f z if z f -1 ran f 0 1 0 = z 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 1 0
444 ovif2 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 1 0 = if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 1 1 f b 2 vol * f -1 ran f 0 0
445 266 267 ifeq12d f dom 1 b vol * f -1 ran f 0 0 if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 1 1 f b 2 vol * f -1 ran f 0 0 = if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
446 444 445 syl5eq f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 1 0 = if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
447 446 mpteq2dv f dom 1 b vol * f -1 ran f 0 0 z 1 f b 2 vol * f -1 ran f 0 if z f -1 ran f 0 1 0 = z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
448 443 447 eqtrd f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f z if z f -1 ran f 0 1 0 = z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
449 eqid z if z f -1 ran f 0 1 0 = z if z f -1 ran f 0 1 0
450 449 i1f1 f -1 ran f 0 dom vol vol f -1 ran f 0 z if z f -1 ran f 0 1 0 dom 1
451 247 252 450 syl2anc f dom 1 z if z f -1 ran f 0 1 0 dom 1
452 451 ad2antrr f dom 1 b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 0 dom 1
453 452 264 i1fmulc f dom 1 b vol * f -1 ran f 0 0 × 1 f b 2 vol * f -1 ran f 0 × f z if z f -1 ran f 0 1 0 dom 1
454 448 453 eqeltrrd f dom 1 b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
455 i1fsub f dom 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
456 233 454 455 syl2anc f dom 1 b vol * f -1 ran f 0 0 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
457 itg1cl f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
458 456 457 syl f dom 1 b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
459 458 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
460 318 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1
461 itg1cl z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
462 460 461 syl f dom 1 b < 1 f b vol * f -1 ran f 0 0 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
463 simplrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 b < 1 f
464 simpr f dom 1 b b
465 8 adantr f dom 1 b 1 f
466 97 a1i f dom 1 b 2 +
467 464 465 466 ltdiv1d f dom 1 b b < 1 f b 2 < 1 f 2
468 recn b b
469 468 2halvesd b b 2 + b 2 = b
470 469 oveq1d b b 2 + b 2 - b 2 = b b 2
471 468 halfcld b b 2
472 471 471 pncand b b 2 + b 2 - b 2 = b 2
473 470 472 eqtr3d b b b 2 = b 2
474 473 breq1d b b b 2 < 1 f 2 b 2 < 1 f 2
475 474 adantl f dom 1 b b b 2 < 1 f 2 b 2 < 1 f 2
476 rehalfcl b b 2
477 476 adantl f dom 1 b b 2
478 8 rehalfcld f dom 1 1 f 2
479 478 adantr f dom 1 b 1 f 2
480 464 477 479 ltsubaddd f dom 1 b b b 2 < 1 f 2 b < 1 f 2 + b 2
481 467 475 480 3bitr2d f dom 1 b b < 1 f b < 1 f 2 + b 2
482 481 adantr f dom 1 b vol * f -1 ran f 0 0 b < 1 f b < 1 f 2 + b 2
483 482 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 b < 1 f b < 1 f 2 + b 2
484 463 483 mpbid f dom 1 b < 1 f b vol * f -1 ran f 0 0 b < 1 f 2 + b 2
485 452 264 itg1mulc f dom 1 b vol * f -1 ran f 0 0 1 × 1 f b 2 vol * f -1 ran f 0 × f z if z f -1 ran f 0 1 0 = 1 f b 2 vol * f -1 ran f 0 1 z if z f -1 ran f 0 1 0
486 448 fveq2d f dom 1 b vol * f -1 ran f 0 0 1 × 1 f b 2 vol * f -1 ran f 0 × f z if z f -1 ran f 0 1 0 = 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
487 449 itg11 f -1 ran f 0 dom vol vol f -1 ran f 0 1 z if z f -1 ran f 0 1 0 = vol f -1 ran f 0
488 247 252 487 syl2anc f dom 1 1 z if z f -1 ran f 0 1 0 = vol f -1 ran f 0
489 488 oveq2d f dom 1 1 f b 2 vol * f -1 ran f 0 1 z if z f -1 ran f 0 1 0 = 1 f b 2 vol * f -1 ran f 0 vol f -1 ran f 0
490 489 ad2antrr f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 1 z if z f -1 ran f 0 1 0 = 1 f b 2 vol * f -1 ran f 0 vol f -1 ran f 0
491 252 recnd f dom 1 vol f -1 ran f 0
492 491 ad2antrr f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0
493 265 492 mulcomd f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 vol f -1 ran f 0 = vol f -1 ran f 0 1 f b 2 vol * f -1 ran f 0
494 249 ad2antrr f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 = vol * f -1 ran f 0
495 494 oveq1d f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 1 f b = vol * f -1 ran f 0 1 f b
496 259 382 mulcomd f dom 1 b vol * f -1 ran f 0 0 vol * f -1 ran f 0 1 f b = 1 f b vol * f -1 ran f 0
497 495 496 eqtrd f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 1 f b = 1 f b vol * f -1 ran f 0
498 497 oveq1d f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 = 1 f b vol * f -1 ran f 0 2 vol * f -1 ran f 0
499 492 382 384 263 divassd f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 = vol f -1 ran f 0 1 f b 2 vol * f -1 ran f 0
500 382 257 259 261 262 divcan5rd f dom 1 b vol * f -1 ran f 0 0 1 f b vol * f -1 ran f 0 2 vol * f -1 ran f 0 = 1 f b 2
501 498 499 500 3eqtr3d f dom 1 b vol * f -1 ran f 0 0 vol f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 = 1 f b 2
502 490 493 501 3eqtrd f dom 1 b vol * f -1 ran f 0 0 1 f b 2 vol * f -1 ran f 0 1 z if z f -1 ran f 0 1 0 = 1 f b 2
503 485 486 502 3eqtr3d f dom 1 b vol * f -1 ran f 0 0 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f b 2
504 503 oveq2d f dom 1 b vol * f -1 ran f 0 0 1 f 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f 1 f b 2
505 itg1sub f dom 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
506 233 454 505 syl2anc f dom 1 b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f 1 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
507 8 recnd f dom 1 1 f
508 507 ad2antrr f dom 1 b vol * f -1 ran f 0 0 1 f
509 468 ad2antlr f dom 1 b vol * f -1 ran f 0 0 b
510 508 509 257 261 divsubdird f dom 1 b vol * f -1 ran f 0 0 1 f b 2 = 1 f 2 b 2
511 510 oveq2d f dom 1 b vol * f -1 ran f 0 0 1 f 1 f b 2 = 1 f 1 f 2 b 2
512 507 adantr f dom 1 b 1 f
513 512 halfcld f dom 1 b 1 f 2
514 471 adantl f dom 1 b b 2
515 512 513 514 subsubd f dom 1 b 1 f 1 f 2 b 2 = 1 f - 1 f 2 + b 2
516 515 adantr f dom 1 b vol * f -1 ran f 0 0 1 f 1 f 2 b 2 = 1 f - 1 f 2 + b 2
517 507 2halvesd f dom 1 1 f 2 + 1 f 2 = 1 f
518 517 oveq1d f dom 1 1 f 2 + 1 f 2 - 1 f 2 = 1 f 1 f 2
519 507 halfcld f dom 1 1 f 2
520 519 519 pncand f dom 1 1 f 2 + 1 f 2 - 1 f 2 = 1 f 2
521 518 520 eqtr3d f dom 1 1 f 1 f 2 = 1 f 2
522 521 oveq1d f dom 1 1 f - 1 f 2 + b 2 = 1 f 2 + b 2
523 522 ad2antrr f dom 1 b vol * f -1 ran f 0 0 1 f - 1 f 2 + b 2 = 1 f 2 + b 2
524 511 516 523 3eqtrrd f dom 1 b vol * f -1 ran f 0 0 1 f 2 + b 2 = 1 f 1 f b 2
525 504 506 524 3eqtr4d f dom 1 b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f 2 + b 2
526 525 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f 2 + b 2
527 484 526 breqtrrd f dom 1 b < 1 f b vol * f -1 ran f 0 0 b < 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
528 456 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1
529 id f dom 1 b vol * f -1 ran f 0 0 f dom 1 b vol * f -1 ran f 0 0
530 529 adantlrl f dom 1 b < 1 f b vol * f -1 ran f 0 0 f dom 1 b vol * f -1 ran f 0 0
531 233 36 sylan f dom 1 b vol * f -1 ran f 0 0 z f z
532 264 adantr f dom 1 b vol * f -1 ran f 0 0 z 1 f b 2 vol * f -1 ran f 0
533 531 532 resubcld f dom 1 b vol * f -1 ran f 0 0 z f z 1 f b 2 vol * f -1 ran f 0
534 533 leidd f dom 1 b vol * f -1 ran f 0 0 z f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0
535 534 adantr f dom 1 b vol * f -1 ran f 0 0 z 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0
536 285 breq2d 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0
537 536 adantl f dom 1 b vol * f -1 ran f 0 0 z 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0
538 535 537 mpbird f dom 1 b vol * f -1 ran f 0 0 z 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
539 533 adantr f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0
540 48 a1i f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 0
541 48 a1i f dom 1 b vol * f -1 ran f 0 0 z 0
542 533 541 ltnled f dom 1 b vol * f -1 ran f 0 0 z f z 1 f b 2 vol * f -1 ran f 0 < 0 ¬ 0 f z 1 f b 2 vol * f -1 ran f 0
543 542 biimpar f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 < 0
544 539 540 543 ltled f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
545 iffalse ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
546 545 breq2d ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 0
547 546 adantl f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 0
548 544 547 mpbird f dom 1 b vol * f -1 ran f 0 0 z ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
549 538 548 pm2.61dan f dom 1 b vol * f -1 ran f 0 0 z f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
550 530 549 sylan f dom 1 b < 1 f b vol * f -1 ran f 0 0 z f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
551 550 adantr f dom 1 b < 1 f b vol * f -1 ran f 0 0 z z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
552 iftrue z f -1 ran f 0 if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 1 f b 2 vol * f -1 ran f 0
553 552 oveq2d z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = f z 1 f b 2 vol * f -1 ran f 0
554 iba z f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0
555 554 bicomd z f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0
556 555 ifbid z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
557 553 556 breq12d z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
558 557 adantl f dom 1 b < 1 f b vol * f -1 ran f 0 0 z z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 1 f b 2 vol * f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
559 551 558 mpbird f dom 1 b < 1 f b vol * f -1 ran f 0 0 z z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
560 35 ad2antrr f dom 1 b < 1 f b vol * f -1 ran f 0 0 f :
561 170 eleq2d f : z f -1 ran f 0 z f -1 ran f f -1 0
562 eldif z f -1 ran f f -1 0 z f -1 ran f ¬ z f -1 0
563 561 562 bitrdi f : z f -1 ran f 0 z f -1 ran f ¬ z f -1 0
564 563 notbid f : ¬ z f -1 ran f 0 ¬ z f -1 ran f ¬ z f -1 0
565 564 adantr f : z ¬ z f -1 ran f 0 ¬ z f -1 ran f ¬ z f -1 0
566 pm4.53 ¬ z f -1 ran f ¬ z f -1 0 ¬ z f -1 ran f z f -1 0
567 207 eleq2d f : z f -1 ran f z
568 567 biimpar f : z z f -1 ran f
569 568 pm2.24d f : z ¬ z f -1 ran f f z = 0
570 181 simplbda f Fn z f -1 0 f z = 0
571 570 ex f Fn z f -1 0 f z = 0
572 180 571 syl f : z f -1 0 f z = 0
573 572 adantr f : z z f -1 0 f z = 0
574 569 573 jaod f : z ¬ z f -1 ran f z f -1 0 f z = 0
575 566 574 syl5bi f : z ¬ z f -1 ran f ¬ z f -1 0 f z = 0
576 565 575 sylbid f : z ¬ z f -1 ran f 0 f z = 0
577 576 imp f : z ¬ z f -1 ran f 0 f z = 0
578 560 577 sylanl1 f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z = 0
579 578 oveq1d f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z 0 = 0 0
580 579 224 eqtrdi f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z 0 = 0
581 580 30 eqbrtrdi f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z 0 0
582 iffalse ¬ z f -1 ran f 0 if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = 0
583 582 oveq2d ¬ z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = f z 0
584 289 288 sylbir ¬ 0 f z 1 f b 2 vol * f -1 ran f 0 ¬ z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
585 584 olcs ¬ z f -1 ran f 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 0
586 583 585 breq12d ¬ z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 0 0
587 586 adantl f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 f z 0 0
588 581 587 mpbird f dom 1 b < 1 f b vol * f -1 ran f 0 0 z ¬ z f -1 ran f 0 f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
589 559 588 pm2.61dan f dom 1 b < 1 f b vol * f -1 ran f 0 0 z f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
590 589 ralrimiva f dom 1 b < 1 f b vol * f -1 ran f 0 0 z f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
591 63 a1i f dom 1 b < 1 f b vol * f -1 ran f 0 0 V
592 ovex f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
593 592 a1i f dom 1 b < 1 f b vol * f -1 ran f 0 0 z f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
594 422 a1i f dom 1 b < 1 f b vol * f -1 ran f 0 0 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 V
595 fvex f z V
596 595 a1i f dom 1 b < 1 f b vol * f -1 ran f 0 0 z f z V
597 199 105 ifex if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
598 597 a1i f dom 1 b < 1 f b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 V
599 70 ad2antrr f dom 1 b < 1 f b vol * f -1 ran f 0 0 f = z f z
600 eqidd f dom 1 b < 1 f b vol * f -1 ran f 0 0 z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
601 591 596 598 599 600 offval2 f dom 1 b < 1 f b vol * f -1 ran f 0 0 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 = z f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0
602 eqidd f dom 1 b < 1 f b vol * f -1 ran f 0 0 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
603 591 593 594 601 602 ofrfval2 f dom 1 b < 1 f b vol * f -1 ran f 0 0 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 f z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 z f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
604 590 603 mpbird f dom 1 b < 1 f b vol * f -1 ran f 0 0 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 f z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
605 itg1le f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 dom 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 dom 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 f z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
606 528 460 604 605 syl3anc f dom 1 b < 1 f b vol * f -1 ran f 0 0 1 f f z if z f -1 ran f 0 1 f b 2 vol * f -1 ran f 0 0 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
607 436 459 462 527 606 ltletrd f dom 1 b < 1 f b vol * f -1 ran f 0 0 b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
608 607 adantllr f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
609 608 adantlll F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
610 fvex 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 V
611 eqeq1 a = 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 a = 1 g 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
612 611 anbi2d a = 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 y + z if g z = 0 0 g z + y f F a = 1 g y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
613 612 rexbidv a = 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g g dom 1 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g
614 breq2 a = 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 b < a b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
615 613 614 anbi12d a = 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a g dom 1 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0
616 610 615 spcev g dom 1 y + z if g z = 0 0 g z + y f F 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 = 1 g b < 1 z if 0 f z 1 f b 2 vol * f -1 ran f 0 z f -1 ran f 0 f z 1 f b 2 vol * f -1 ran f 0 0 a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
617 435 609 616 syl2anc F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b vol * f -1 ran f 0 0 a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
618 192 617 pm2.61dane F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
619 618 expr F : 0 +∞ f dom 1 f f F s = 1 f b < 1 f b a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
620 619 adantllr F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
621 620 adantr F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ b a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
622 157 621 mpd F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f b −∞ a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
623 139 622 pm2.61dane F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
624 623 ex F : 0 +∞ b * f dom 1 f f F s = 1 f b < 1 f a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
625 94 624 sylbid F : 0 +∞ b * f dom 1 f f F s = 1 f b < s a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
626 625 imp F : 0 +∞ b * f dom 1 f f F s = 1 f b < s a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
627 626 an32s F : 0 +∞ b * b < s f dom 1 f f F s = 1 f a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
628 627 rexlimdvaa F : 0 +∞ b * b < s f dom 1 f f F s = 1 f a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
629 628 expimpd F : 0 +∞ b * b < s f dom 1 f f F s = 1 f a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
630 629 ancomsd F : 0 +∞ b * f dom 1 f f F s = 1 f b < s a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
631 630 exlimdv F : 0 +∞ b * s f dom 1 f f F s = 1 f b < s a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
632 eqeq1 x = s x = 1 f s = 1 f
633 632 anbi2d x = s f f F x = 1 f f f F s = 1 f
634 633 rexbidv x = s f dom 1 f f F x = 1 f f dom 1 f f F s = 1 f
635 634 rexab s x | f dom 1 f f F x = 1 f b < s s f dom 1 f f F s = 1 f b < s
636 eqeq1 x = a x = 1 g a = 1 g
637 636 anbi2d x = a y + z if g z = 0 0 g z + y f F x = 1 g y + z if g z = 0 0 g z + y f F a = 1 g
638 637 rexbidv x = a g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g
639 638 rexab a x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g b < a a g dom 1 y + z if g z = 0 0 g z + y f F a = 1 g b < a
640 631 635 639 3imtr4g F : 0 +∞ b * s x | f dom 1 f f F x = 1 f b < s a x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g b < a
641 92 640 sylbid F : 0 +∞ b * b < sup x | f dom 1 f f F x = 1 f * < a x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g b < a
642 641 impr F : 0 +∞ b * b < sup x | f dom 1 f f F x = 1 f * < a x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g b < a
643 6 15 89 642 eqsupd F : 0 +∞ sup x | g dom 1 y + z if g z = 0 0 g z + y f F x = 1 g * < = sup x | f dom 1 f f F x = 1 f * <
644 4 643 syl5eq F : 0 +∞ sup L * < = sup x | f dom 1 f f F x = 1 f * <
645 3 644 eqtr4d F : 0 +∞ 2 F = sup L * <