Mathbox for Brendan Leahy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anclem6 Structured version   Visualization version   Unicode version

Theorem ftc1anclem6 32086
 Description: Lemma for ftc1anc 32089- 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 . (Contributed by Brendan Leahy, 31-May-2018.)
Hypotheses
Ref Expression
ftc1anc.g
ftc1anc.a
ftc1anc.b
ftc1anc.le
ftc1anc.s
ftc1anc.d
ftc1anc.i
ftc1anc.f
Assertion
Ref Expression
ftc1anclem6
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,   ,,   ,,,,
Allowed substitution hints:   (,)

Proof of Theorem ftc1anclem6
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rphalfcl 11350 . . 3
2 ftc1anc.g . . . 4
3 ftc1anc.a . . . 4
4 ftc1anc.b . . . 4
5 ftc1anc.le . . . 4
6 ftc1anc.s . . . 4
7 ftc1anc.d . . . 4
8 ftc1anc.i . . . 4
9 ftc1anc.f . . . 4
102, 3, 4, 5, 6, 7, 8, 9ftc1anclem5 32085 . . 3
111, 10sylan2 482 . 2
12 eqid 2471 . . . . 5
13 ax-icn 9616 . . . . . . . 8
14 ine0 10075 . . . . . . . 8
1513, 14reccli 10359 . . . . . . 7
1615a1i 11 . . . . . 6
179ffvelrnda 6037 . . . . . 6
189feqmptd 5932 . . . . . . 7
1918, 8eqeltrrd 2550 . . . . . 6
20 divrec2 10309 . . . . . . . . . 10
2113, 14, 20mp3an23 1382 . . . . . . . . 9
2217, 21syl 17 . . . . . . . 8
2322mpteq2dva 4482 . . . . . . 7
24 iblmbf 22804 . . . . . . . . 9 MblFn
2519, 24syl 17 . . . . . . . 8 MblFn
26 fveq2 5879 . . . . . . . . . . . . . . . . 17
2726fveq2d 5883 . . . . . . . . . . . . . . . 16
2827cbvmptv 4488 . . . . . . . . . . . . . . 15
2928eleq1i 2540 . . . . . . . . . . . . . 14 MblFn MblFn
3017recld 13334 . . . . . . . . . . . . . . . . 17
3130recnd 9687 . . . . . . . . . . . . . . . 16
3231adantlr 729 . . . . . . . . . . . . . . 15 MblFn
3329biimpri 211 . . . . . . . . . . . . . . . 16 MblFn MblFn
3433adantl 473 . . . . . . . . . . . . . . 15 MblFn MblFn
3532, 34mbfneg 22685 . . . . . . . . . . . . . 14 MblFn MblFn
3629, 35sylan2b 483 . . . . . . . . . . . . 13 MblFn MblFn
379ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . 20
3837recld 13334 . . . . . . . . . . . . . . . . . . 19
3938recnd 9687 . . . . . . . . . . . . . . . . . 18
4039negnegd 9996 . . . . . . . . . . . . . . . . 17
4140mpteq2dva 4482 . . . . . . . . . . . . . . . 16
4241, 28syl6eqr 2523 . . . . . . . . . . . . . . 15
4342adantr 472 . . . . . . . . . . . . . 14 MblFn
44 negex 9893 . . . . . . . . . . . . . . . 16
4544a1i 11 . . . . . . . . . . . . . . 15 MblFn
4627negeqd 9889 . . . . . . . . . . . . . . . . . . 19
4746cbvmptv 4488 . . . . . . . . . . . . . . . . . 18
4847eleq1i 2540 . . . . . . . . . . . . . . . . 17 MblFn MblFn
4948biimpi 199 . . . . . . . . . . . . . . . 16 MblFn MblFn
5049adantl 473 . . . . . . . . . . . . . . 15 MblFn MblFn
5145, 50mbfneg 22685 . . . . . . . . . . . . . 14 MblFn MblFn
5243, 51eqeltrrd 2550 . . . . . . . . . . . . 13 MblFn MblFn
5336, 52impbida 850 . . . . . . . . . . . 12 MblFn MblFn
54 divcl 10298 . . . . . . . . . . . . . . . . . 18
55 imre 13248 . . . . . . . . . . . . . . . . . 18
5654, 55syl 17 . . . . . . . . . . . . . . . . 17
5713, 14, 56mp3an23 1382 . . . . . . . . . . . . . . . 16
5813, 14, 54mp3an23 1382 . . . . . . . . . . . . . . . . . . 19
59 mulneg1 10076 . . . . . . . . . . . . . . . . . . 19
6013, 58, 59sylancr 676 . . . . . . . . . . . . . . . . . 18
61 divcan2 10300 . . . . . . . . . . . . . . . . . . . 20
6213, 14, 61mp3an23 1382 . . . . . . . . . . . . . . . . . . 19
6362negeqd 9889 . . . . . . . . . . . . . . . . . 18
6460, 63eqtrd 2505 . . . . . . . . . . . . . . . . 17
6564fveq2d 5883 . . . . . . . . . . . . . . . 16
66 reneg 13265 . . . . . . . . . . . . . . . 16
6757, 65, 663eqtrd 2509 . . . . . . . . . . . . . . 15
6817, 67syl 17 . . . . . . . . . . . . . 14
6968mpteq2dva 4482 . . . . . . . . . . . . 13
7069eleq1d 2533 . . . . . . . . . . . 12 MblFn MblFn
7153, 70bitr4d 264 . . . . . . . . . . 11 MblFn MblFn
72 imval 13247 . . . . . . . . . . . . . 14
7317, 72syl 17 . . . . . . . . . . . . 13
7473mpteq2dva 4482 . . . . . . . . . . . 12
7574eleq1d 2533 . . . . . . . . . . 11 MblFn MblFn
7671, 75anbi12d 725 . . . . . . . . . 10 MblFn MblFn MblFn MblFn
77 ancom 457 . . . . . . . . . 10 MblFn MblFn MblFn MblFn
7876, 77syl6bb 269 . . . . . . . . 9 MblFn MblFn MblFn MblFn
7917ismbfcn2 22674 . . . . . . . . 9 MblFn MblFn MblFn
8017, 58syl 17 . . . . . . . . . 10
8180ismbfcn2 22674 . . . . . . . . 9 MblFn MblFn MblFn
8278, 79, 813bitr4d 293 . . . . . . . 8 MblFn MblFn
8325, 82mpbid 215 . . . . . . 7 MblFn
8423, 83eqeltrrd 2550 . . . . . 6 MblFn
8516, 17, 19, 84iblmulc2nc 32071 . . . . 5
86 mulcl 9641 . . . . . . 7
8715, 17, 86sylancr 676 . . . . . 6
88 eqid 2471 . . . . . 6
8987, 88fmptd 6061 . . . . 5
9012, 3, 4, 5, 6, 7, 85, 89ftc1anclem5 32085 . . . 4
911, 90sylan2 482 . . 3
929ffvelrnda 6037 . . . . . . . . . . . . 13
93 0cnd 9654 . . . . . . . . . . . . 13
9492, 93ifclda 3904 . . . . . . . . . . . 12
95 imval 13247 . . . . . . . . . . . 12
9694, 95syl 17 . . . . . . . . . . 11
97 fveq2 5879 . . . . . . . . . . . . . . . . . 18
9897oveq2d 6324 . . . . . . . . . . . . . . . . 17
99 ovex 6336 . . . . . . . . . . . . . . . . 17
10098, 88, 99fvmpt 5963 . . . . . . . . . . . . . . . 16
101100adantl 473 . . . . . . . . . . . . . . 15
102 divrec2 10309 . . . . . . . . . . . . . . . . 17
10313, 14, 102mp3an23 1382 . . . . . . . . . . . . . . . 16
10492, 103syl 17 . . . . . . . . . . . . . . 15
105101, 104eqtr4d 2508 . . . . . . . . . . . . . 14
106105ifeq1da 3902 . . . . . . . . . . . . 13
107 ovif 6392 . . . . . . . . . . . . . 14
10813, 14div0i 10363 . . . . . . . . . . . . . . 15
109 ifeq2 3877 . . . . . . . . . . . . . . 15
110108, 109ax-mp 5 . . . . . . . . . . . . . 14
111107, 110eqtri 2493 . . . . . . . . . . . . 13
112106, 111syl6eqr 2523 . . . . . . . . . . . 12
113112fveq2d 5883 . . . . . . . . . . 11
11496, 113eqtr4d 2508 . . . . . . . . . 10
115114oveq1d 6323 . . . . . . . . 9
116115fveq2d 5883 . . . . . . . 8
117116mpteq2dv 4483 . . . . . . 7
118117fveq2d 5883 . . . . . 6
119118breq1d 4405 . . . . 5
120119rexbidv 2892 . . . 4
12291, 121mpbird 240 . 2
123 reeanv 2944 . . 3
124 eleq1 2537 . . . . . . . . . . . . . . . . . . 19
125 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
126124, 125ifbieq1d 3895 . . . . . . . . . . . . . . . . . 18
127126fveq2d 5883 . . . . . . . . . . . . . . . . 17
128 eqid 2471 . . . . . . . . . . . . . . . . 17
129 fvex 5889 . . . . . . . . . . . . . . . . 17
130127, 128, 129fvmpt 5963 . . . . . . . . . . . . . . . 16
131130oveq1d 6323 . . . . . . . . . . . . . . 15
132131fveq2d 5883 . . . . . . . . . . . . . 14
133132mpteq2ia 4478 . . . . . . . . . . . . 13
134133fveq2i 5882 . . . . . . . . . . . 12
135 rembl 22572 . . . . . . . . . . . . . . . . . . 19
136135a1i 11 . . . . . . . . . . . . . . . . . 18
137 0cnd 9654 . . . . . . . . . . . . . . . . . . . 20
13837, 137ifclda 3904 . . . . . . . . . . . . . . . . . . 19
139138adantr 472 . . . . . . . . . . . . . . . . . 18
140 eldifn 3545 . . . . . . . . . . . . . . . . . . . 20
141140adantl 473 . . . . . . . . . . . . . . . . . . 19
142141iffalsed 3883 . . . . . . . . . . . . . . . . . 18
1439feqmptd 5932 . . . . . . . . . . . . . . . . . . . 20
144 iftrue 3878 . . . . . . . . . . . . . . . . . . . . 21
145144mpteq2ia 4478 . . . . . . . . . . . . . . . . . . . 20
146143, 145syl6eqr 2523 . . . . . . . . . . . . . . . . . . 19
147146, 8eqeltrrd 2550 . . . . . . . . . . . . . . . . . 18
1487, 136, 139, 142, 147iblss2 22842 . . . . . . . . . . . . . . . . 17
149138adantr 472 . . . . . . . . . . . . . . . . . 18
150149iblcn 22835 . . . . . . . . . . . . . . . . 17
151148, 150mpbid 215 . . . . . . . . . . . . . . . 16
152151simpld 466 . . . . . . . . . . . . . . 15
153149recld 13334 . . . . . . . . . . . . . . . 16
154153, 128fmptd 6061 . . . . . . . . . . . . . . 15
155152, 154jca 541 . . . . . . . . . . . . . 14
156 ftc1anclem4 32084 . . . . . . . . . . . . . . 15
1571563expb 1232 . . . . . . . . . . . . . 14
158155, 157sylan2 482 . . . . . . . . . . . . 13
159158ancoms 460 . . . . . . . . . . . 12
160134, 159syl5eqelr 2554 . . . . . . . . . . 11
161126fveq2d 5883 . . . . . . . . . . . . . . . . 17
162 eqid 2471 . . . . . . . . . . . . . . . . 17
163 fvex 5889 . . . . . . . . . . . . . . . . 17
164161, 162, 163fvmpt 5963 . . . . . . . . . . . . . . . 16
165164oveq1d 6323 . . . . . . . . . . . . . . 15
166165fveq2d 5883 . . . . . . . . . . . . . 14
167166mpteq2ia 4478 . . . . . . . . . . . . 13
168167fveq2i 5882 . . . . . . . . . . . 12
169151simprd 470 . . . . . . . . . . . . . . 15
170138imcld 13335 . . . . . . . . . . . . . . . . 17
171170adantr 472 . . . . . . . . . . . . . . . 16
172171, 162fmptd 6061 . . . . . . . . . . . . . . 15
173169, 172jca 541 . . . . . . . . . . . . . 14
174 ftc1anclem4 32084 . . . . . . . . . . . . . . 15
1751743expb 1232 . . . . . . . . . . . . . 14
176173, 175sylan2 482 . . . . . . . . . . . . 13
177176ancoms 460 . . . . . . . . . . . 12
178168, 177syl5eqelr 2554 . . . . . . . . . . 11
179160, 178anim12dan 855 . . . . . . . . . 10
1801rpred 11364 . . . . . . . . . . 11
181180, 180jca 541 . . . . . . . . . 10
182 lt2add 10120 . . . . . . . . . 10
183179, 181, 182syl2an 485 . . . . . . . . 9
184183an32s 821 . . . . . . . 8
18594recld 13334 . . . . . . . . . . . . . . . . . . . . 21
186185recnd 9687 . . . . . . . . . . . . . . . . . . . 20
187 i1ff 22713 . . . . . . . . . . . . . . . . . . . . . 22
188187ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . 21
189188recnd 9687 . . . . . . . . . . . . . . . . . . . 20
190 subcl 9894 . . . . . . . . . . . . . . . . . . . 20
191186, 189, 190syl2an 485 . . . . . . . . . . . . . . . . . . 19
192191anassrs 660 . . . . . . . . . . . . . . . . . 18
193192adantlrr 735 . . . . . . . . . . . . . . . . 17
19494imcld 13335 . . . . . . . . . . . . . . . . . . . . . 22
195194recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
196 i1ff 22713 . . . . . . . . . . . . . . . . . . . . . . 23
197196ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . 22
198197recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
199 subcl 9894 . . . . . . . . . . . . . . . . . . . . 21
200195, 198, 199syl2an 485 . . . . . . . . . . . . . . . . . . . 20
201200anassrs 660 . . . . . . . . . . . . . . . . . . 19
202 mulcl 9641 . . . . . . . . . . . . . . . . . . 19
20313, 201, 202sylancr 676 . . . . . . . . . . . . . . . . . 18
204203adantlrl 734 . . . . . . . . . . . . . . . . 17
205193, 204addcld 9680 . . . . . . . . . . . . . . . 16
206205abscld 13575 . . . . . . . . . . . . . . 15
207206rexrd 9708 . . . . . . . . . . . . . 14
208205absge0d 13583 . . . . . . . . . . . . . 14
209 elxrge0 11767 . . . . . . . . . . . . . 14
210207, 208, 209sylanbrc 677 . . . . . . . . . . . . 13
211 eqid 2471 . . . . . . . . . . . . 13
212210, 211fmptd 6061 . . . . . . . . . . . 12
213 icossicc 11746 . . . . . . . . . . . . . . 15
214 ge0addcl 11770 . . . . . . . . . . . . . . 15
215213, 214sseldi 3416 . . . . . . . . . . . . . 14
216215adantl 473 . . . . . . . . . . . . 13
217192abscld 13575 . . . . . . . . . . . . . . . 16
218192absge0d 13583 . . . . . . . . . . . . . . . 16
219 elrege0 11764 . . . . . . . . . . . . . . . 16
220217, 218, 219sylanbrc 677 . . . . . . . . . . . . . . 15
221 eqid 2471 . . . . . . . . . . . . . . 15
222220, 221fmptd 6061 . . . . . . . . . . . . . 14
223222adantrr 731 . . . . . . . . . . . . 13
224201abscld 13575 . . . . . . . . . . . . . . . 16
225201absge0d 13583 . . . . . . . . . . . . . . . 16
226 elrege0 11764 . . . . . . . . . . . . . . . 16
227224, 225, 226sylanbrc 677 . . . . . . . . . . . . . . 15
228 eqid 2471 . . . . . . . . . . . . . . 15
229227, 228fmptd 6061 . . . . . . . . . . . . . 14
230229adantrl 730 . . . . . . . . . . . . 13
231 reex 9648 . . . . . . . . . . . . . 14
232231a1i 11 . . . . . . . . . . . . 13
233 inidm 3632 . . . . . . . . . . . . 13
234216, 223, 230, 232, 232, 233off 6565 . . . . . . . . . . . 12
235193, 204abstrid 13595 . . . . . . . . . . . . . 14
236235ralrimiva 2809 . . . . . . . . . . . . 13
237 ovex 6336 . . . . . . . . . . . . . . 15
238237a1i 11 . . . . . . . . . . . . . 14
239 eqidd 2472 . . . . . . . . . . . . . 14
240 fvex 5889 . . . . . . . . . . . . . . . 16
241240a1i 11 . . . . . . . . . . . . . . 15
242 fvex 5889 . . . . . . . . . . . . . . . 16
243242a1i 11 . . . . . . . . . . . . . . 15
244 eqidd 2472 . . . . . . . . . . . . . . 15
245 absmul 13434 . . . . . . . . . . . . . . . . . . 19
24613, 201, 245sylancr 676 . . . . . . . . . . . . . . . . . 18
247 absi 13426 . . . . . . . . . . . . . . . . . . . 20
248247oveq1i 6318 . . . . . . . . . . . . . . . . . . 19
249224recnd 9687 . . . . . . . . . . . . . . . . . . . 20
250249mulid2d 9679 . . . . . . . . . . . . . . . . . . 19
251248, 250syl5eq 2517 . . . . . . . . . . . . . . . . . 18
252246, 251eqtr2d 2506 . . . . . . . . . . . . . . . . 17
253252mpteq2dva 4482 . . . . . . . . . . . . . . . 16
254253adantrl 730 . . . . . . . . . . . . . . 15
255232, 241, 243, 244, 254offval2 6567 . . . . . . . . . . . . . 14
256232, 206, 238, 239, 255ofrfval2 6568 . . . . . . . . . . . . 13
257236, 256mpbird 240 . . . . . . . . . . . 12
258 itg2le 22776 . . . . . . . . . . . 12
259212, 234, 257, 258syl3anc 1292 . . . . . . . . . . 11
260 eqidd 2472 . . . . . . . . . . . . . . 15
261 absf 13477 . . . . . . . . . . . . . . . . 17
262261a1i 11 . . . . . . . . . . . . . . . 16
263262feqmptd 5932 . . . . . . . . . . . . . . 15
264 fveq2 5879 . . . . . . . . . . . . . . 15
265192, 260, 263, 264fmptco 6072 . . . . . . . . . . . . . 14
266 resubcl 9958 . . . . . . . . . . . . . . . . . 18
267185, 188, 266syl2an 485 . . . . . . . . . . . . . . . . 17
268267anassrs 660 . . . . . . . . . . . . . . . 16
269 eqid 2471 . . . . . . . . . . . . . . . 16
270268, 269fmptd 6061 . . . . . . . . . . . . . . 15
271135a1i 11 . . . . . . . . . . . . . . . 16
272 iunin2 4333 . . . . . . . . . . . . . . . . . . . . 21
273 imaiun 6168 . . . . . . . . . . . . . . . . . . . . . . 23
274 iunid 4324 . . . . . . . . . . . . . . . . . . . . . . . 24
275274imaeq2i 5172 . . . . . . . . . . . . . . . . . . . . . . 23
276273, 275eqtr3i 2495 . . . . . . . . . . . . . . . . . . . . . 22
277276ineq2i 3622 . . . . . . . . . . . . . . . . . . . . 21
278272, 277eqtri 2493 . . . . . . . . . . . . . . . . . . . 20
279 cnvimass 5194 . . . . . . . . . . . . . . . . . . . . . . 23
280 ovex 6336 . . . . . . . . . . . . . . . . . . . . . . . 24
281280, 269dmmpti 5717 . . . . . . . . . . . . . . . . . . . . . . 23
282279, 281sseqtri 3450 . . . . . . . . . . . . . . . . . . . . . 22
283 cnvimarndm 5195 . . . . . . . . . . . . . . . . . . . . . . 23
284 fdm 5745 . . . . . . . . . . . . . . . . . . . . . . . 24
285187, 284syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
286283, 285syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . 22
287282, 286syl5sseqr 3467 . . . . . . . . . . . . . . . . . . . . 21
288 df-ss 3404 . . . . . . . . . . . . . . . . . . . . 21
289287, 288sylib 201 . . . . . . . . . . . . . . . . . . . 20
290278, 289syl5eq 2517 . . . . . . . . . . . . . . . . . . 19
291290ad2antlr 741 . . . . . . . . . . . . . . . . . 18