Metamath Proof Explorer


Theorem ftc1anclem6

Description: Lemma for ftc1anc - construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of Fremlin5 p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued F . (Contributed by Brendan Leahy, 31-May-2018)

Ref Expression
Hypotheses ftc1anc.g G = x A B A x F t dt
ftc1anc.a φ A
ftc1anc.b φ B
ftc1anc.le φ A B
ftc1anc.s φ A B D
ftc1anc.d φ D
ftc1anc.i φ F 𝐿 1
ftc1anc.f φ F : D
Assertion ftc1anclem6 φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < Y

Proof

Step Hyp Ref Expression
1 ftc1anc.g G = x A B A x F t dt
2 ftc1anc.a φ A
3 ftc1anc.b φ B
4 ftc1anc.le φ A B
5 ftc1anc.s φ A B D
6 ftc1anc.d φ D
7 ftc1anc.i φ F 𝐿 1
8 ftc1anc.f φ F : D
9 rphalfcl Y + Y 2 +
10 1 2 3 4 5 6 7 8 ftc1anclem5 φ Y 2 + f dom 1 2 t if t D F t 0 f t < Y 2
11 9 10 sylan2 φ Y + f dom 1 2 t if t D F t 0 f t < Y 2
12 eqid x A B A x y D 1 i F y t dt = x A B A x y D 1 i F y t dt
13 ax-icn i
14 ine0 i 0
15 13 14 reccli 1 i
16 15 a1i φ 1 i
17 8 ffvelrnda φ y D F y
18 8 feqmptd φ F = y D F y
19 18 7 eqeltrrd φ y D F y 𝐿 1
20 divrec2 F y i i 0 F y i = 1 i F y
21 13 14 20 mp3an23 F y F y i = 1 i F y
22 17 21 syl φ y D F y i = 1 i F y
23 22 mpteq2dva φ y D F y i = y D 1 i F y
24 iblmbf y D F y 𝐿 1 y D F y MblFn
25 19 24 syl φ y D F y MblFn
26 2fveq3 y = x F y = F x
27 26 cbvmptv y D F y = x D F x
28 27 eleq1i y D F y MblFn x D F x MblFn
29 17 recld φ y D F y
30 29 recnd φ y D F y
31 30 adantlr φ x D F x MblFn y D F y
32 28 biimpri x D F x MblFn y D F y MblFn
33 32 adantl φ x D F x MblFn y D F y MblFn
34 31 33 mbfneg φ x D F x MblFn y D F y MblFn
35 28 34 sylan2b φ y D F y MblFn y D F y MblFn
36 8 ffvelrnda φ x D F x
37 36 recld φ x D F x
38 37 recnd φ x D F x
39 38 negnegd φ x D F x = F x
40 39 mpteq2dva φ x D F x = x D F x
41 40 27 eqtr4di φ x D F x = y D F y
42 41 adantr φ y D F y MblFn x D F x = y D F y
43 negex F x V
44 43 a1i φ y D F y MblFn x D F x V
45 26 negeqd y = x F y = F x
46 45 cbvmptv y D F y = x D F x
47 46 eleq1i y D F y MblFn x D F x MblFn
48 47 biimpi y D F y MblFn x D F x MblFn
49 48 adantl φ y D F y MblFn x D F x MblFn
50 44 49 mbfneg φ y D F y MblFn x D F x MblFn
51 42 50 eqeltrrd φ y D F y MblFn y D F y MblFn
52 35 51 impbida φ y D F y MblFn y D F y MblFn
53 divcl F y i i 0 F y i
54 imre F y i F y i = i F y i
55 53 54 syl F y i i 0 F y i = i F y i
56 13 14 55 mp3an23 F y F y i = i F y i
57 13 14 53 mp3an23 F y F y i
58 mulneg1 i F y i i F y i = i F y i
59 13 57 58 sylancr F y i F y i = i F y i
60 divcan2 F y i i 0 i F y i = F y
61 13 14 60 mp3an23 F y i F y i = F y
62 61 negeqd F y i F y i = F y
63 59 62 eqtrd F y i F y i = F y
64 63 fveq2d F y i F y i = F y
65 reneg F y F y = F y
66 56 64 65 3eqtrd F y F y i = F y
67 17 66 syl φ y D F y i = F y
68 67 mpteq2dva φ y D F y i = y D F y
69 68 eleq1d φ y D F y i MblFn y D F y MblFn
70 52 69 bitr4d φ y D F y MblFn y D F y i MblFn
71 imval F y F y = F y i
72 17 71 syl φ y D F y = F y i
73 72 mpteq2dva φ y D F y = y D F y i
74 73 eleq1d φ y D F y MblFn y D F y i MblFn
75 70 74 anbi12d φ y D F y MblFn y D F y MblFn y D F y i MblFn y D F y i MblFn
76 ancom y D F y i MblFn y D F y i MblFn y D F y i MblFn y D F y i MblFn
77 75 76 bitrdi φ y D F y MblFn y D F y MblFn y D F y i MblFn y D F y i MblFn
78 17 ismbfcn2 φ y D F y MblFn y D F y MblFn y D F y MblFn
79 17 57 syl φ y D F y i
80 79 ismbfcn2 φ y D F y i MblFn y D F y i MblFn y D F y i MblFn
81 77 78 80 3bitr4d φ y D F y MblFn y D F y i MblFn
82 25 81 mpbid φ y D F y i MblFn
83 23 82 eqeltrrd φ y D 1 i F y MblFn
84 16 17 19 83 iblmulc2nc φ y D 1 i F y 𝐿 1
85 mulcl 1 i F y 1 i F y
86 15 17 85 sylancr φ y D 1 i F y
87 86 fmpttd φ y D 1 i F y : D
88 12 2 3 4 5 6 84 87 ftc1anclem5 φ Y 2 + g dom 1 2 t if t D y D 1 i F y t 0 g t < Y 2
89 9 88 sylan2 φ Y + g dom 1 2 t if t D y D 1 i F y t 0 g t < Y 2
90 8 ffvelrnda φ t D F t
91 0cnd φ ¬ t D 0
92 90 91 ifclda φ if t D F t 0
93 imval if t D F t 0 if t D F t 0 = if t D F t 0 i
94 92 93 syl φ if t D F t 0 = if t D F t 0 i
95 fveq2 y = t F y = F t
96 95 oveq2d y = t 1 i F y = 1 i F t
97 eqid y D 1 i F y = y D 1 i F y
98 ovex 1 i F t V
99 96 97 98 fvmpt t D y D 1 i F y t = 1 i F t
100 99 adantl φ t D y D 1 i F y t = 1 i F t
101 divrec2 F t i i 0 F t i = 1 i F t
102 13 14 101 mp3an23 F t F t i = 1 i F t
103 90 102 syl φ t D F t i = 1 i F t
104 100 103 eqtr4d φ t D y D 1 i F y t = F t i
105 104 ifeq1da φ if t D y D 1 i F y t 0 = if t D F t i 0
106 ovif if t D F t 0 i = if t D F t i 0 i
107 13 14 div0i 0 i = 0
108 ifeq2 0 i = 0 if t D F t i 0 i = if t D F t i 0
109 107 108 ax-mp if t D F t i 0 i = if t D F t i 0
110 106 109 eqtri if t D F t 0 i = if t D F t i 0
111 105 110 eqtr4di φ if t D y D 1 i F y t 0 = if t D F t 0 i
112 111 fveq2d φ if t D y D 1 i F y t 0 = if t D F t 0 i
113 94 112 eqtr4d φ if t D F t 0 = if t D y D 1 i F y t 0
114 113 fvoveq1d φ if t D F t 0 g t = if t D y D 1 i F y t 0 g t
115 114 mpteq2dv φ t if t D F t 0 g t = t if t D y D 1 i F y t 0 g t
116 115 fveq2d φ 2 t if t D F t 0 g t = 2 t if t D y D 1 i F y t 0 g t
117 116 breq1d φ 2 t if t D F t 0 g t < Y 2 2 t if t D y D 1 i F y t 0 g t < Y 2
118 117 rexbidv φ g dom 1 2 t if t D F t 0 g t < Y 2 g dom 1 2 t if t D y D 1 i F y t 0 g t < Y 2
119 118 adantr φ Y + g dom 1 2 t if t D F t 0 g t < Y 2 g dom 1 2 t if t D y D 1 i F y t 0 g t < Y 2
120 89 119 mpbird φ Y + g dom 1 2 t if t D F t 0 g t < Y 2
121 reeanv f dom 1 g dom 1 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 f dom 1 2 t if t D F t 0 f t < Y 2 g dom 1 2 t if t D F t 0 g t < Y 2
122 eleq1w x = t x D t D
123 fveq2 x = t F x = F t
124 122 123 ifbieq1d x = t if x D F x 0 = if t D F t 0
125 124 fveq2d x = t if x D F x 0 = if t D F t 0
126 eqid x if x D F x 0 = x if x D F x 0
127 fvex if t D F t 0 V
128 125 126 127 fvmpt t x if x D F x 0 t = if t D F t 0
129 128 fvoveq1d t x if x D F x 0 t f t = if t D F t 0 f t
130 129 mpteq2ia t x if x D F x 0 t f t = t if t D F t 0 f t
131 130 fveq2i 2 t x if x D F x 0 t f t = 2 t if t D F t 0 f t
132 rembl dom vol
133 132 a1i φ dom vol
134 0cnd φ ¬ x D 0
135 36 134 ifclda φ if x D F x 0
136 135 adantr φ x D if x D F x 0
137 eldifn x D ¬ x D
138 137 adantl φ x D ¬ x D
139 138 iffalsed φ x D if x D F x 0 = 0
140 8 feqmptd φ F = x D F x
141 iftrue x D if x D F x 0 = F x
142 141 mpteq2ia x D if x D F x 0 = x D F x
143 140 142 eqtr4di φ F = x D if x D F x 0
144 143 7 eqeltrrd φ x D if x D F x 0 𝐿 1
145 6 133 136 139 144 iblss2 φ x if x D F x 0 𝐿 1
146 135 adantr φ x if x D F x 0
147 146 iblcn φ x if x D F x 0 𝐿 1 x if x D F x 0 𝐿 1 x if x D F x 0 𝐿 1
148 145 147 mpbid φ x if x D F x 0 𝐿 1 x if x D F x 0 𝐿 1
149 148 simpld φ x if x D F x 0 𝐿 1
150 146 recld φ x if x D F x 0
151 150 fmpttd φ x if x D F x 0 :
152 149 151 jca φ x if x D F x 0 𝐿 1 x if x D F x 0 :
153 ftc1anclem4 f dom 1 x if x D F x 0 𝐿 1 x if x D F x 0 : 2 t x if x D F x 0 t f t
154 153 3expb f dom 1 x if x D F x 0 𝐿 1 x if x D F x 0 : 2 t x if x D F x 0 t f t
155 152 154 sylan2 f dom 1 φ 2 t x if x D F x 0 t f t
156 155 ancoms φ f dom 1 2 t x if x D F x 0 t f t
157 131 156 eqeltrrid φ f dom 1 2 t if t D F t 0 f t
158 124 fveq2d x = t if x D F x 0 = if t D F t 0
159 eqid x if x D F x 0 = x if x D F x 0
160 fvex if t D F t 0 V
161 158 159 160 fvmpt t x if x D F x 0 t = if t D F t 0
162 161 fvoveq1d t x if x D F x 0 t g t = if t D F t 0 g t
163 162 mpteq2ia t x if x D F x 0 t g t = t if t D F t 0 g t
164 163 fveq2i 2 t x if x D F x 0 t g t = 2 t if t D F t 0 g t
165 148 simprd φ x if x D F x 0 𝐿 1
166 135 imcld φ if x D F x 0
167 166 adantr φ x if x D F x 0
168 167 fmpttd φ x if x D F x 0 :
169 165 168 jca φ x if x D F x 0 𝐿 1 x if x D F x 0 :
170 ftc1anclem4 g dom 1 x if x D F x 0 𝐿 1 x if x D F x 0 : 2 t x if x D F x 0 t g t
171 170 3expb g dom 1 x if x D F x 0 𝐿 1 x if x D F x 0 : 2 t x if x D F x 0 t g t
172 169 171 sylan2 g dom 1 φ 2 t x if x D F x 0 t g t
173 172 ancoms φ g dom 1 2 t x if x D F x 0 t g t
174 164 173 eqeltrrid φ g dom 1 2 t if t D F t 0 g t
175 157 174 anim12dan φ f dom 1 g dom 1 2 t if t D F t 0 f t 2 t if t D F t 0 g t
176 9 rpred Y + Y 2
177 176 176 jca Y + Y 2 Y 2
178 lt2add 2 t if t D F t 0 f t 2 t if t D F t 0 g t Y 2 Y 2 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2
179 175 177 178 syl2an φ f dom 1 g dom 1 Y + 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2
180 179 an32s φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2
181 92 recld φ if t D F t 0
182 181 recnd φ if t D F t 0
183 i1ff f dom 1 f :
184 183 ffvelrnda f dom 1 t f t
185 184 recnd f dom 1 t f t
186 subcl if t D F t 0 f t if t D F t 0 f t
187 182 185 186 syl2an φ f dom 1 t if t D F t 0 f t
188 187 anassrs φ f dom 1 t if t D F t 0 f t
189 188 adantlrr φ f dom 1 g dom 1 t if t D F t 0 f t
190 92 imcld φ if t D F t 0
191 190 recnd φ if t D F t 0
192 i1ff g dom 1 g :
193 192 ffvelrnda g dom 1 t g t
194 193 recnd g dom 1 t g t
195 subcl if t D F t 0 g t if t D F t 0 g t
196 191 194 195 syl2an φ g dom 1 t if t D F t 0 g t
197 196 anassrs φ g dom 1 t if t D F t 0 g t
198 mulcl i if t D F t 0 g t i if t D F t 0 g t
199 13 197 198 sylancr φ g dom 1 t i if t D F t 0 g t
200 199 adantlrl φ f dom 1 g dom 1 t i if t D F t 0 g t
201 189 200 addcld φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t
202 201 abscld φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t
203 202 rexrd φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t *
204 201 absge0d φ f dom 1 g dom 1 t 0 if t D F t 0 - f t + i if t D F t 0 g t
205 elxrge0 if t D F t 0 - f t + i if t D F t 0 g t 0 +∞ if t D F t 0 - f t + i if t D F t 0 g t * 0 if t D F t 0 - f t + i if t D F t 0 g t
206 203 204 205 sylanbrc φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t 0 +∞
207 206 fmpttd φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t : 0 +∞
208 icossicc 0 +∞ 0 +∞
209 ge0addcl x 0 +∞ y 0 +∞ x + y 0 +∞
210 208 209 sselid x 0 +∞ y 0 +∞ x + y 0 +∞
211 210 adantl φ f dom 1 g dom 1 x 0 +∞ y 0 +∞ x + y 0 +∞
212 188 abscld φ f dom 1 t if t D F t 0 f t
213 188 absge0d φ f dom 1 t 0 if t D F t 0 f t
214 elrege0 if t D F t 0 f t 0 +∞ if t D F t 0 f t 0 if t D F t 0 f t
215 212 213 214 sylanbrc φ f dom 1 t if t D F t 0 f t 0 +∞
216 215 fmpttd φ f dom 1 t if t D F t 0 f t : 0 +∞
217 216 adantrr φ f dom 1 g dom 1 t if t D F t 0 f t : 0 +∞
218 197 abscld φ g dom 1 t if t D F t 0 g t
219 197 absge0d φ g dom 1 t 0 if t D F t 0 g t
220 elrege0 if t D F t 0 g t 0 +∞ if t D F t 0 g t 0 if t D F t 0 g t
221 218 219 220 sylanbrc φ g dom 1 t if t D F t 0 g t 0 +∞
222 221 fmpttd φ g dom 1 t if t D F t 0 g t : 0 +∞
223 222 adantrl φ f dom 1 g dom 1 t if t D F t 0 g t : 0 +∞
224 reex V
225 224 a1i φ f dom 1 g dom 1 V
226 inidm =
227 211 217 223 225 225 226 off φ f dom 1 g dom 1 t if t D F t 0 f t + f t if t D F t 0 g t : 0 +∞
228 189 200 abstrid φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t if t D F t 0 f t + i if t D F t 0 g t
229 228 ralrimiva φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t if t D F t 0 f t + i if t D F t 0 g t
230 ovexd φ f dom 1 g dom 1 t if t D F t 0 f t + i if t D F t 0 g t V
231 eqidd φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t = t if t D F t 0 - f t + i if t D F t 0 g t
232 fvexd φ f dom 1 g dom 1 t if t D F t 0 f t V
233 fvexd φ f dom 1 g dom 1 t i if t D F t 0 g t V
234 eqidd φ f dom 1 g dom 1 t if t D F t 0 f t = t if t D F t 0 f t
235 absmul i if t D F t 0 g t i if t D F t 0 g t = i if t D F t 0 g t
236 13 197 235 sylancr φ g dom 1 t i if t D F t 0 g t = i if t D F t 0 g t
237 absi i = 1
238 237 oveq1i i if t D F t 0 g t = 1 if t D F t 0 g t
239 218 recnd φ g dom 1 t if t D F t 0 g t
240 239 mulid2d φ g dom 1 t 1 if t D F t 0 g t = if t D F t 0 g t
241 238 240 syl5eq φ g dom 1 t i if t D F t 0 g t = if t D F t 0 g t
242 236 241 eqtr2d φ g dom 1 t if t D F t 0 g t = i if t D F t 0 g t
243 242 mpteq2dva φ g dom 1 t if t D F t 0 g t = t i if t D F t 0 g t
244 243 adantrl φ f dom 1 g dom 1 t if t D F t 0 g t = t i if t D F t 0 g t
245 225 232 233 234 244 offval2 φ f dom 1 g dom 1 t if t D F t 0 f t + f t if t D F t 0 g t = t if t D F t 0 f t + i if t D F t 0 g t
246 225 202 230 231 245 ofrfval2 φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t f t if t D F t 0 f t + f t if t D F t 0 g t t if t D F t 0 - f t + i if t D F t 0 g t if t D F t 0 f t + i if t D F t 0 g t
247 229 246 mpbird φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t f t if t D F t 0 f t + f t if t D F t 0 g t
248 itg2le t if t D F t 0 - f t + i if t D F t 0 g t : 0 +∞ t if t D F t 0 f t + f t if t D F t 0 g t : 0 +∞ t if t D F t 0 - f t + i if t D F t 0 g t f t if t D F t 0 f t + f t if t D F t 0 g t 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + f t if t D F t 0 g t
249 207 227 247 248 syl3anc φ f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + f t if t D F t 0 g t
250 absf abs :
251 250 a1i φ f dom 1 abs :
252 251 188 cofmpt φ f dom 1 abs t if t D F t 0 f t = t if t D F t 0 f t
253 resubcl if t D F t 0 f t if t D F t 0 f t
254 181 184 253 syl2an φ f dom 1 t if t D F t 0 f t
255 254 anassrs φ f dom 1 t if t D F t 0 f t
256 255 fmpttd φ f dom 1 t if t D F t 0 f t :
257 132 a1i φ f dom 1 dom vol
258 iunin2 y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 f t -1 x +∞ y ran f f -1 y
259 imaiun f -1 y ran f y = y ran f f -1 y
260 iunid y ran f y = ran f
261 260 imaeq2i f -1 y ran f y = f -1 ran f
262 259 261 eqtr3i y ran f f -1 y = f -1 ran f
263 262 ineq2i t if t D F t 0 f t -1 x +∞ y ran f f -1 y = t if t D F t 0 f t -1 x +∞ f -1 ran f
264 258 263 eqtri y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 f t -1 x +∞ f -1 ran f
265 cnvimass t if t D F t 0 f t -1 x +∞ dom t if t D F t 0 f t
266 ovex if t D F t 0 f t V
267 eqid t if t D F t 0 f t = t if t D F t 0 f t
268 266 267 dmmpti dom t if t D F t 0 f t =
269 265 268 sseqtri t if t D F t 0 f t -1 x +∞
270 cnvimarndm f -1 ran f = dom f
271 183 fdmd f dom 1 dom f =
272 270 271 syl5eq f dom 1 f -1 ran f =
273 269 272 sseqtrrid f dom 1 t if t D F t 0 f t -1 x +∞ f -1 ran f
274 df-ss t if t D F t 0 f t -1 x +∞ f -1 ran f t if t D F t 0 f t -1 x +∞ f -1 ran f = t if t D F t 0 f t -1 x +∞
275 273 274 sylib f dom 1 t if t D F t 0 f t -1 x +∞ f -1 ran f = t if t D F t 0 f t -1 x +∞
276 264 275 syl5eq f dom 1 y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 f t -1 x +∞
277 276 ad2antlr φ f dom 1 x y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 f t -1 x +∞
278 183 frnd f dom 1 ran f
279 278 ad2antlr φ f dom 1 x ran f
280 279 sselda φ f dom 1 x y ran f y
281 181 ad2antrr φ x y if t D F t 0
282 resubcl if t D F t 0 y if t D F t 0 y
283 181 282 sylan φ y if t D F t 0 y
284 283 adantlr φ x y if t D F t 0 y
285 281 284 2thd φ x y if t D F t 0 if t D F t 0 y
286 ltaddsub x y if t D F t 0 x + y < if t D F t 0 x < if t D F t 0 y
287 181 286 syl3an3 x y φ x + y < if t D F t 0 x < if t D F t 0 y
288 287 3comr φ x y x + y < if t D F t 0 x < if t D F t 0 y
289 288 3expa φ x y x + y < if t D F t 0 x < if t D F t 0 y
290 285 289 anbi12d φ x y if t D F t 0 x + y < if t D F t 0 if t D F t 0 y x < if t D F t 0 y
291 readdcl x y x + y
292 291 rexrd x y x + y *
293 292 adantll φ x y x + y *
294 elioopnf x + y * if t D F t 0 x + y +∞ if t D F t 0 x + y < if t D F t 0
295 293 294 syl φ x y if t D F t 0 x + y +∞ if t D F t 0 x + y < if t D F t 0
296 rexr x x *
297 296 ad2antlr φ x y x *
298 elioopnf x * if t D F t 0 y x +∞ if t D F t 0 y x < if t D F t 0 y
299 297 298 syl φ x y if t D F t 0 y x +∞ if t D F t 0 y x < if t D F t 0 y
300 290 295 299 3bitr4rd φ x y if t D F t 0 y x +∞ if t D F t 0 x + y +∞
301 oveq2 f t = y if t D F t 0 f t = if t D F t 0 y
302 301 eleq1d f t = y if t D F t 0 f t x +∞ if t D F t 0 y x +∞
303 302 bibi1d f t = y if t D F t 0 f t x +∞ if t D F t 0 x + y +∞ if t D F t 0 y x +∞ if t D F t 0 x + y +∞
304 300 303 syl5ibrcom φ x y f t = y if t D F t 0 f t x +∞ if t D F t 0 x + y +∞
305 304 pm5.32rd φ x y if t D F t 0 f t x +∞ f t = y if t D F t 0 x + y +∞ f t = y
306 305 adantllr φ f dom 1 x y if t D F t 0 f t x +∞ f t = y if t D F t 0 x + y +∞ f t = y
307 280 306 syldan φ f dom 1 x y ran f if t D F t 0 f t x +∞ f t = y if t D F t 0 x + y +∞ f t = y
308 307 rabbidv φ f dom 1 x y ran f t | if t D F t 0 f t x +∞ f t = y = t | if t D F t 0 x + y +∞ f t = y
309 183 feqmptd f dom 1 f = t f t
310 309 cnveqd f dom 1 f -1 = t f t -1
311 310 imaeq1d f dom 1 f -1 y = t f t -1 y
312 311 ineq2d f dom 1 t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 f t -1 x +∞ t f t -1 y
313 267 mptpreima t if t D F t 0 f t -1 x +∞ = t | if t D F t 0 f t x +∞
314 vex y V
315 eqid t f t = t f t
316 315 mptiniseg y V t f t -1 y = t | f t = y
317 314 316 ax-mp t f t -1 y = t | f t = y
318 313 317 ineq12i t if t D F t 0 f t -1 x +∞ t f t -1 y = t | if t D F t 0 f t x +∞ t | f t = y
319 inrab t | if t D F t 0 f t x +∞ t | f t = y = t | if t D F t 0 f t x +∞ f t = y
320 318 319 eqtri t if t D F t 0 f t -1 x +∞ t f t -1 y = t | if t D F t 0 f t x +∞ f t = y
321 312 320 eqtrdi f dom 1 t if t D F t 0 f t -1 x +∞ f -1 y = t | if t D F t 0 f t x +∞ f t = y
322 321 ad3antlr φ f dom 1 x y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t | if t D F t 0 f t x +∞ f t = y
323 311 ineq2d f dom 1 t if t D F t 0 -1 x + y +∞ f -1 y = t if t D F t 0 -1 x + y +∞ t f t -1 y
324 eqid t if t D F t 0 = t if t D F t 0
325 324 mptpreima t if t D F t 0 -1 x + y +∞ = t | if t D F t 0 x + y +∞
326 325 317 ineq12i t if t D F t 0 -1 x + y +∞ t f t -1 y = t | if t D F t 0 x + y +∞ t | f t = y
327 inrab t | if t D F t 0 x + y +∞ t | f t = y = t | if t D F t 0 x + y +∞ f t = y
328 326 327 eqtri t if t D F t 0 -1 x + y +∞ t f t -1 y = t | if t D F t 0 x + y +∞ f t = y
329 323 328 eqtrdi f dom 1 t if t D F t 0 -1 x + y +∞ f -1 y = t | if t D F t 0 x + y +∞ f t = y
330 329 ad3antlr φ f dom 1 x y ran f t if t D F t 0 -1 x + y +∞ f -1 y = t | if t D F t 0 x + y +∞ f t = y
331 308 322 330 3eqtr4d φ f dom 1 x y ran f t if t D F t 0 f t -1 x +∞ f -1 y = t if t D F t 0 -1 x + y +∞ f -1 y
332 331 iuneq2dv φ f dom 1 x y ran f t if t D F t 0 f t -1 x +∞ f -1 y = y ran f t if t D F t 0 -1 x + y +∞ f -1 y
333 277 332 eqtr3d φ f dom 1 x t if t D F t 0 f t -1 x +∞ = y ran f t if t D F t 0 -1 x + y +∞ f -1 y
334 i1frn f dom 1 ran f Fin
335 334 adantl φ f dom 1 ran f Fin
336 92 adantr φ t D if t D F t 0
337 eldifn t D ¬ t D
338 337 adantl φ t D ¬ t D
339 338 iffalsed φ t D if t D F t 0 = 0
340 8 feqmptd φ F = t D F t
341 iftrue t D if t D F t 0 = F t
342 341 mpteq2ia t D if t D F t 0 = t D F t
343 340 342 eqtr4di φ F = t D if t D F t 0
344 iblmbf F 𝐿 1 F MblFn
345 7 344 syl φ F MblFn
346 343 345 eqeltrrd φ t D if t D F t 0 MblFn
347 6 133 336 339 346 mbfss φ t if t D F t 0 MblFn
348 92 adantr φ t if t D F t 0
349 348 ismbfcn2 φ t if t D F t 0 MblFn t if t D F t 0 MblFn t if t D F t 0 MblFn
350 347 349 mpbid φ t if t D F t 0 MblFn t if t D F t 0 MblFn
351 350 simpld φ t if t D F t 0 MblFn
352 181 adantr φ t if t D F t 0
353 352 fmpttd φ t if t D F t 0 :
354 mbfima t if t D F t 0 MblFn t if t D F t 0 : t if t D F t 0 -1 x + y +∞ dom vol
355 351 353 354 syl2anc φ t if t D F t 0 -1 x + y +∞ dom vol
356 i1fima f dom 1 f -1 y dom vol
357 inmbl t if t D F t 0 -1 x + y +∞ dom vol f -1 y dom vol t if t D F t 0 -1 x + y +∞ f -1 y dom vol
358 355 356 357 syl2an φ f dom 1 t if t D F t 0 -1 x + y +∞ f -1 y dom vol
359 358 ralrimivw φ f dom 1 y ran f t if t D F t 0 -1 x + y +∞ f -1 y dom vol
360 finiunmbl ran f Fin y ran f t if t D F t 0 -1 x + y +∞ f -1 y dom vol y ran f t if t D F t 0 -1 x + y +∞ f -1 y dom vol
361 335 359 360 syl2anc φ f dom 1 y ran f t if t D F t 0 -1 x + y +∞ f -1 y dom vol
362 361 adantr φ f dom 1 x y ran f t if t D F t 0 -1 x + y +∞ f -1 y dom vol
363 333 362 eqeltrd φ f dom 1 x t if t D F t 0 f t -1 x +∞ dom vol
364 iunin2 y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 f t -1 −∞ x y ran f f -1 y
365 262 ineq2i t if t D F t 0 f t -1 −∞ x y ran f f -1 y = t if t D F t 0 f t -1 −∞ x f -1 ran f
366 364 365 eqtri y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 f t -1 −∞ x f -1 ran f
367 cnvimass t if t D F t 0 f t -1 −∞ x dom t if t D F t 0 f t
368 367 268 sseqtri t if t D F t 0 f t -1 −∞ x
369 368 272 sseqtrrid f dom 1 t if t D F t 0 f t -1 −∞ x f -1 ran f
370 df-ss t if t D F t 0 f t -1 −∞ x f -1 ran f t if t D F t 0 f t -1 −∞ x f -1 ran f = t if t D F t 0 f t -1 −∞ x
371 369 370 sylib f dom 1 t if t D F t 0 f t -1 −∞ x f -1 ran f = t if t D F t 0 f t -1 −∞ x
372 366 371 syl5eq f dom 1 y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 f t -1 −∞ x
373 372 ad2antlr φ f dom 1 x y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 f t -1 −∞ x
374 284 281 2thd φ x y if t D F t 0 y if t D F t 0
375 ltsubadd if t D F t 0 y x if t D F t 0 y < x if t D F t 0 < x + y
376 181 375 syl3an1 φ y x if t D F t 0 y < x if t D F t 0 < x + y
377 376 3expa φ y x if t D F t 0 y < x if t D F t 0 < x + y
378 377 an32s φ x y if t D F t 0 y < x if t D F t 0 < x + y
379 374 378 anbi12d φ x y if t D F t 0 y if t D F t 0 y < x if t D F t 0 if t D F t 0 < x + y
380 elioomnf x * if t D F t 0 y −∞ x if t D F t 0 y if t D F t 0 y < x
381 297 380 syl φ x y if t D F t 0 y −∞ x if t D F t 0 y if t D F t 0 y < x
382 elioomnf x + y * if t D F t 0 −∞ x + y if t D F t 0 if t D F t 0 < x + y
383 293 382 syl φ x y if t D F t 0 −∞ x + y if t D F t 0 if t D F t 0 < x + y
384 379 381 383 3bitr4d φ x y if t D F t 0 y −∞ x if t D F t 0 −∞ x + y
385 301 eleq1d f t = y if t D F t 0 f t −∞ x if t D F t 0 y −∞ x
386 385 bibi1d f t = y if t D F t 0 f t −∞ x if t D F t 0 −∞ x + y if t D F t 0 y −∞ x if t D F t 0 −∞ x + y
387 384 386 syl5ibrcom φ x y f t = y if t D F t 0 f t −∞ x if t D F t 0 −∞ x + y
388 387 pm5.32rd φ x y if t D F t 0 f t −∞ x f t = y if t D F t 0 −∞ x + y f t = y
389 388 adantllr φ f dom 1 x y if t D F t 0 f t −∞ x f t = y if t D F t 0 −∞ x + y f t = y
390 280 389 syldan φ f dom 1 x y ran f if t D F t 0 f t −∞ x f t = y if t D F t 0 −∞ x + y f t = y
391 390 rabbidv φ f dom 1 x y ran f t | if t D F t 0 f t −∞ x f t = y = t | if t D F t 0 −∞ x + y f t = y
392 311 ineq2d f dom 1 t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 f t -1 −∞ x t f t -1 y
393 267 mptpreima t if t D F t 0 f t -1 −∞ x = t | if t D F t 0 f t −∞ x
394 393 317 ineq12i t if t D F t 0 f t -1 −∞ x t f t -1 y = t | if t D F t 0 f t −∞ x t | f t = y
395 inrab t | if t D F t 0 f t −∞ x t | f t = y = t | if t D F t 0 f t −∞ x f t = y
396 394 395 eqtri t if t D F t 0 f t -1 −∞ x t f t -1 y = t | if t D F t 0 f t −∞ x f t = y
397 392 396 eqtrdi f dom 1 t if t D F t 0 f t -1 −∞ x f -1 y = t | if t D F t 0 f t −∞ x f t = y
398 397 ad3antlr φ f dom 1 x y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t | if t D F t 0 f t −∞ x f t = y
399 311 ineq2d f dom 1 t if t D F t 0 -1 −∞ x + y f -1 y = t if t D F t 0 -1 −∞ x + y t f t -1 y
400 324 mptpreima t if t D F t 0 -1 −∞ x + y = t | if t D F t 0 −∞ x + y
401 400 317 ineq12i t if t D F t 0 -1 −∞ x + y t f t -1 y = t | if t D F t 0 −∞ x + y t | f t = y
402 inrab t | if t D F t 0 −∞ x + y t | f t = y = t | if t D F t 0 −∞ x + y f t = y
403 401 402 eqtri t if t D F t 0 -1 −∞ x + y t f t -1 y = t | if t D F t 0 −∞ x + y f t = y
404 399 403 eqtrdi f dom 1 t if t D F t 0 -1 −∞ x + y f -1 y = t | if t D F t 0 −∞ x + y f t = y
405 404 ad3antlr φ f dom 1 x y ran f t if t D F t 0 -1 −∞ x + y f -1 y = t | if t D F t 0 −∞ x + y f t = y
406 391 398 405 3eqtr4d φ f dom 1 x y ran f t if t D F t 0 f t -1 −∞ x f -1 y = t if t D F t 0 -1 −∞ x + y f -1 y
407 406 iuneq2dv φ f dom 1 x y ran f t if t D F t 0 f t -1 −∞ x f -1 y = y ran f t if t D F t 0 -1 −∞ x + y f -1 y
408 373 407 eqtr3d φ f dom 1 x t if t D F t 0 f t -1 −∞ x = y ran f t if t D F t 0 -1 −∞ x + y f -1 y
409 mbfima t if t D F t 0 MblFn t if t D F t 0 : t if t D F t 0 -1 −∞ x + y dom vol
410 351 353 409 syl2anc φ t if t D F t 0 -1 −∞ x + y dom vol
411 inmbl t if t D F t 0 -1 −∞ x + y dom vol f -1 y dom vol t if t D F t 0 -1 −∞ x + y f -1 y dom vol
412 410 356 411 syl2an φ f dom 1 t if t D F t 0 -1 −∞ x + y f -1 y dom vol
413 412 ralrimivw φ f dom 1 y ran f t if t D F t 0 -1 −∞ x + y f -1 y dom vol
414 finiunmbl ran f Fin y ran f t if t D F t 0 -1 −∞ x + y f -1 y dom vol y ran f t if t D F t 0 -1 −∞ x + y f -1 y dom vol
415 335 413 414 syl2anc φ f dom 1 y ran f t if t D F t 0 -1 −∞ x + y f -1 y dom vol
416 415 adantr φ f dom 1 x y ran f t if t D F t 0 -1 −∞ x + y f -1 y dom vol
417 408 416 eqeltrd φ f dom 1 x t if t D F t 0 f t -1 −∞ x dom vol
418 256 257 363 417 ismbf2d φ f dom 1 t if t D F t 0 f t MblFn
419 ftc1anclem1 t if t D F t 0 f t : t if t D F t 0 f t MblFn abs t if t D F t 0 f t MblFn
420 256 418 419 syl2anc φ f dom 1 abs t if t D F t 0 f t MblFn
421 252 420 eqeltrrd φ f dom 1 t if t D F t 0 f t MblFn
422 421 adantrr φ f dom 1 g dom 1 t if t D F t 0 f t MblFn
423 157 adantrr φ f dom 1 g dom 1 2 t if t D F t 0 f t
424 174 adantrl φ f dom 1 g dom 1 2 t if t D F t 0 g t
425 422 217 423 223 424 itg2addnc φ f dom 1 g dom 1 2 t if t D F t 0 f t + f t if t D F t 0 g t = 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
426 249 425 breqtrd φ f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
427 426 adantlr φ Y + f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
428 itg2cl t if t D F t 0 - f t + i if t D F t 0 g t : 0 +∞ 2 t if t D F t 0 - f t + i if t D F t 0 g t *
429 207 428 syl φ f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t *
430 429 adantlr φ Y + f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t *
431 readdcl 2 t if t D F t 0 f t 2 t if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
432 157 174 431 syl2an φ f dom 1 φ g dom 1 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
433 432 anandis φ f dom 1 g dom 1 2 t if t D F t 0 f t + 2 t if t D F t 0 g t
434 433 rexrd φ f dom 1 g dom 1 2 t if t D F t 0 f t + 2 t if t D F t 0 g t *
435 434 adantlr φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t + 2 t if t D F t 0 g t *
436 9 9 rpaddcld Y + Y 2 + Y 2 +
437 436 rpxrd Y + Y 2 + Y 2 *
438 437 ad2antlr φ Y + f dom 1 g dom 1 Y 2 + Y 2 *
439 xrlelttr 2 t if t D F t 0 - f t + i if t D F t 0 g t * 2 t if t D F t 0 f t + 2 t if t D F t 0 g t * Y 2 + Y 2 * 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2 2 t if t D F t 0 - f t + i if t D F t 0 g t < Y 2 + Y 2
440 430 435 438 439 syl3anc φ Y + f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2 2 t if t D F t 0 - f t + i if t D F t 0 g t < Y 2 + Y 2
441 427 440 mpand φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t + 2 t if t D F t 0 g t < Y 2 + Y 2 2 t if t D F t 0 - f t + i if t D F t 0 g t < Y 2 + Y 2
442 180 441 syld φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 2 t if t D F t 0 - f t + i if t D F t 0 g t < Y 2 + Y 2
443 mulcl i if t D F t 0 i if t D F t 0
444 13 191 443 sylancr φ i if t D F t 0
445 182 444 jca φ if t D F t 0 i if t D F t 0
446 mulcl i g t i g t
447 13 194 446 sylancr g dom 1 t i g t
448 185 447 anim12i f dom 1 t g dom 1 t f t i g t
449 448 anandirs f dom 1 g dom 1 t f t i g t
450 addsub4 if t D F t 0 i if t D F t 0 f t i g t if t D F t 0 + i if t D F t 0 - f t + i g t = if t D F t 0 f t + i if t D F t 0 - i g t
451 445 449 450 syl2an φ f dom 1 g dom 1 t if t D F t 0 + i if t D F t 0 - f t + i g t = if t D F t 0 f t + i if t D F t 0 - i g t
452 451 anassrs φ f dom 1 g dom 1 t if t D F t 0 + i if t D F t 0 - f t + i g t = if t D F t 0 f t + i if t D F t 0 - i g t
453 92 replimd φ if t D F t 0 = if t D F t 0 + i if t D F t 0
454 453 ad2antrr φ f dom 1 g dom 1 t if t D F t 0 = if t D F t 0 + i if t D F t 0
455 454 oveq1d φ f dom 1 g dom 1 t if t D F t 0 f t + i g t = if t D F t 0 + i if t D F t 0 - f t + i g t
456 194 adantll f dom 1 g dom 1 t g t
457 subdi i if t D F t 0 g t i if t D F t 0 g t = i if t D F t 0 i g t
458 13 191 456 457 mp3an3an φ f dom 1 g dom 1 t i if t D F t 0 g t = i if t D F t 0 i g t
459 458 anassrs φ f dom 1 g dom 1 t i if t D F t 0 g t = i if t D F t 0 i g t
460 459 oveq2d φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t = if t D F t 0 f t + i if t D F t 0 - i g t
461 452 455 460 3eqtr4rd φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t = if t D F t 0 f t + i g t
462 461 fveq2d φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t = if t D F t 0 f t + i g t
463 462 mpteq2dva φ f dom 1 g dom 1 t if t D F t 0 - f t + i if t D F t 0 g t = t if t D F t 0 f t + i g t
464 463 fveq2d φ f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t = 2 t if t D F t 0 f t + i g t
465 464 adantlr φ Y + f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t = 2 t if t D F t 0 f t + i g t
466 rpcn Y + Y
467 466 2halvesd Y + Y 2 + Y 2 = Y
468 467 ad2antlr φ Y + f dom 1 g dom 1 Y 2 + Y 2 = Y
469 465 468 breq12d φ Y + f dom 1 g dom 1 2 t if t D F t 0 - f t + i if t D F t 0 g t < Y 2 + Y 2 2 t if t D F t 0 f t + i g t < Y
470 442 469 sylibd φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 2 t if t D F t 0 f t + i g t < Y
471 470 reximdvva φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t < Y 2 2 t if t D F t 0 g t < Y 2 f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < Y
472 121 471 syl5bir φ Y + f dom 1 2 t if t D F t 0 f t < Y 2 g dom 1 2 t if t D F t 0 g t < Y 2 f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < Y
473 11 120 472 mp2and φ Y + f dom 1 g dom 1 2 t if t D F t 0 f t + i g t < Y