Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfi1fseqlem4 Structured version   Unicode version

Theorem mbfi1fseqlem4 19602
 Description: Lemma for mbfi1fseq 19605. This lemma is not as interesting as it is long - it is simply checking that is in fact a sequence of simple functions, by verifying that its range is in (which is to say, the numbers from to in increments of ), and also that the preimage of each point is measurable, because it is equal to for and for . (Contributed by Mario Carneiro, 16-Aug-2014.)
Hypotheses
Ref Expression
mbfi1fseq.1 MblFn
mbfi1fseq.2
mbfi1fseq.3
mbfi1fseq.4
Assertion
Ref Expression
mbfi1fseqlem4
Distinct variable groups:   ,,,   ,   ,   ,,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem mbfi1fseqlem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 9073 . . . . 5
21mptex 5958 . . . 4
3 mbfi1fseq.4 . . . 4
42, 3fnmpti 5565 . . 3
54a1i 11 . 2
6 mbfi1fseq.1 . . . . . 6 MblFn
7 mbfi1fseq.2 . . . . . 6
8 mbfi1fseq.3 . . . . . 6
96, 7, 8, 3mbfi1fseqlem3 19601 . . . . 5
10 elfznn0 11075 . . . . . . . . 9
1110nn0red 10267 . . . . . . . 8
12 2nn 10125 . . . . . . . . . 10
13 nnnn0 10220 . . . . . . . . . 10
14 nnexpcl 11386 . . . . . . . . . 10
1512, 13, 14sylancr 645 . . . . . . . . 9
1615adantl 453 . . . . . . . 8
17 nndivre 10027 . . . . . . . 8
1811, 16, 17syl2anr 465 . . . . . . 7
19 eqid 2435 . . . . . . 7
2018, 19fmptd 5885 . . . . . 6
21 frn 5589 . . . . . 6
2220, 21syl 16 . . . . 5
23 fss 5591 . . . . 5
249, 22, 23syl2anc 643 . . . 4
25 fzfid 11304 . . . . . 6
26 ffn 5583 . . . . . . . 8
2720, 26syl 16 . . . . . . 7
28 dffn4 5651 . . . . . . 7
2927, 28sylib 189 . . . . . 6
30 fofi 7384 . . . . . 6
3125, 29, 30syl2anc 643 . . . . 5
32 frn 5589 . . . . . 6
339, 32syl 16 . . . . 5
34 ssfi 7321 . . . . 5
3531, 33, 34syl2anc 643 . . . 4
366, 7, 8, 3mbfi1fseqlem2 19600 . . . . . . . . . . . . . 14
3736fveq1d 5722 . . . . . . . . . . . . 13
3837ad2antlr 708 . . . . . . . . . . . 12
39 simpr 448 . . . . . . . . . . . . 13
40 ovex 6098 . . . . . . . . . . . . . . 15
41 vex 2951 . . . . . . . . . . . . . . 15
4240, 41ifex 3789 . . . . . . . . . . . . . 14
43 c0ex 9077 . . . . . . . . . . . . . 14
4442, 43ifex 3789 . . . . . . . . . . . . 13
45 eqid 2435 . . . . . . . . . . . . . 14
4645fvmpt2 5804 . . . . . . . . . . . . 13
4739, 44, 46sylancl 644 . . . . . . . . . . . 12
4838, 47eqtrd 2467 . . . . . . . . . . 11
4948adantlr 696 . . . . . . . . . 10
5049eqeq1d 2443 . . . . . . . . 9
51 eldifsni 3920 . . . . . . . . . . . . 13
5251ad2antlr 708 . . . . . . . . . . . 12
53 neeq1 2606 . . . . . . . . . . . 12
5452, 53syl5ibrcom 214 . . . . . . . . . . 11
55 iffalse 3738 . . . . . . . . . . . 12
5655necon1ai 2640 . . . . . . . . . . 11
5754, 56syl6 31 . . . . . . . . . 10
5857pm4.71rd 617 . . . . . . . . 9
59 iftrue 3737 . . . . . . . . . . . 12
6059eqeq1d 2443 . . . . . . . . . . 11
61 simpllr 736 . . . . . . . . . . . . . . . . . 18
6261nnred 10007 . . . . . . . . . . . . . . . . 17
6362adantr 452 . . . . . . . . . . . . . . . 16
64 0re 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
65 pnfxr 10705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
66 icossre 10983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6764, 65, 66mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26
68 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
69 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
707, 68, 69syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7167, 70sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . . . 25
72 nnnn0 10220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
73 nnexpcl 11386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7412, 72, 73sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7574ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7675nnred 10007 . . . . . . . . . . . . . . . . . . . . . . . . 25
7771, 76remulcld 9108 . . . . . . . . . . . . . . . . . . . . . . . 24
78 reflcl 11197 . . . . . . . . . . . . . . . . . . . . . . . 24
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
8079, 75nndivred 10040 . . . . . . . . . . . . . . . . . . . . . 22
8180ralrimivva 2790 . . . . . . . . . . . . . . . . . . . . 21
828fmpt2 6410 . . . . . . . . . . . . . . . . . . . . 21
8381, 82sylib 189 . . . . . . . . . . . . . . . . . . . 20
84 fovrn 6208 . . . . . . . . . . . . . . . . . . . 20
8583, 84syl3an1 1217 . . . . . . . . . . . . . . . . . . 19
86853expa 1153 . . . . . . . . . . . . . . . . . 18
8786adantlr 696 . . . . . . . . . . . . . . . . 17
8887adantr 452 . . . . . . . . . . . . . . . 16
89 lemin 10771 . . . . . . . . . . . . . . . 16
9063, 88, 63, 89syl3anc 1184 . . . . . . . . . . . . . . 15
91 ifcl 3767 . . . . . . . . . . . . . . . . . 18
9288, 63, 91syl2anc 643 . . . . . . . . . . . . . . . . 17
9392, 63letri3d 9207 . . . . . . . . . . . . . . . 16
94 simpr 448 . . . . . . . . . . . . . . . . 17
9594eqeq2d 2446 . . . . . . . . . . . . . . . 16
96 min2 10769 . . . . . . . . . . . . . . . . . 18
9788, 63, 96syl2anc 643 . . . . . . . . . . . . . . . . 17
9897biantrurd 495 . . . . . . . . . . . . . . . 16
9993, 95, 983bitr4d 277 . . . . . . . . . . . . . . 15
10063leidd 9585 . . . . . . . . . . . . . . . 16
101100biantrud 494 . . . . . . . . . . . . . . 15
10290, 99, 1013bitr4d 277 . . . . . . . . . . . . . 14
103 breq1 4207 . . . . . . . . . . . . . . 15
1047adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
105104ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . 22
106 elrege0 10999 . . . . . . . . . . . . . . . . . . . . . 22
107105, 106sylib 189 . . . . . . . . . . . . . . . . . . . . 21
108107simpld 446 . . . . . . . . . . . . . . . . . . . 20
109108adantlr 696 . . . . . . . . . . . . . . . . . . 19
11061, 15syl 16 . . . . . . . . . . . . . . . . . . . 20
111110nnred 10007 . . . . . . . . . . . . . . . . . . 19
112109, 111remulcld 9108 . . . . . . . . . . . . . . . . . 18
113 reflcl 11197 . . . . . . . . . . . . . . . . . 18
114112, 113syl 16 . . . . . . . . . . . . . . . . 17
115110nngt0d 10035 . . . . . . . . . . . . . . . . 17
116 lemuldiv 9881 . . . . . . . . . . . . . . . . 17
11762, 114, 111, 115, 116syl112anc 1188 . . . . . . . . . . . . . . . 16
118 lemul1 9854 . . . . . . . . . . . . . . . . . 18
11962, 109, 111, 115, 118syl112anc 1188 . . . . . . . . . . . . . . . . 17
120 nnmulcl 10015 . . . . . . . . . . . . . . . . . . . . 21
12115, 120mpdan 650 . . . . . . . . . . . . . . . . . . . 20
12261, 121syl 16 . . . . . . . . . . . . . . . . . . 19
123122nnzd 10366 . . . . . . . . . . . . . . . . . 18
124 flge 11206 . . . . . . . . . . . . . . . . . 18
125112, 123, 124syl2anc 643 . . . . . . . . . . . . . . . . 17
126119, 125bitrd 245 . . . . . . . . . . . . . . . 16
127 simpr 448 . . . . . . . . . . . . . . . . . 18
128 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23
129128fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 22
130 simpl 444 . . . . . . . . . . . . . . . . . . . . . . 23
131130oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22
132129, 131oveq12d 6091 . . . . . . . . . . . . . . . . . . . . 21
133132fveq2d 5724 . . . . . . . . . . . . . . . . . . . 20
134133, 131oveq12d 6091 . . . . . . . . . . . . . . . . . . 19
135 ovex 6098 . . . . . . . . . . . . . . . . . . 19
136134, 8, 135ovmpt2a 6196 . . . . . . . . . . . . . . . . . 18
13761, 127, 136syl2anc 643 . . . . . . . . . . . . . . . . 17
138137breq2d 4216 . . . . . . . . . . . . . . . 16
139117, 126, 1383bitr4d 277 . . . . . . . . . . . . . . 15
140103, 139sylan9bbr 682 . . . . . . . . . . . . . 14
141127adantr 452 . . . . . . . . . . . . . . . 16
142 iftrue 3737 . . . . . . . . . . . . . . . . 17
143142adantl 453 . . . . . . . . . . . . . . . 16
144141, 143eleqtrrd 2512 . . . . . . . . . . . . . . 15
145144biantrurd 495 . . . . . . . . . . . . . 14
146102, 140, 1453bitr2d 273 . . . . . . . . . . . . 13
14733ssdifssd 3477 . . . . . . . . . . . . . . . . . . 19
148147sselda 3340 . . . . . . . . . . . . . . . . . 18
14919rnmpt 5108 . . . . . . . . . . . . . . . . . . . . 21
150149abeq2i 2542 . . . . . . . . . . . . . . . . . . . 20
151 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . . . . . . 26
152151adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
153152zcnd 10368 . . . . . . . . . . . . . . . . . . . . . . . 24
15415ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25
155154nncnd 10008 . . . . . . . . . . . . . . . . . . . . . . . 24
156154nnne0d 10036 . . . . . . . . . . . . . . . . . . . . . . . 24
157153, 155, 156divcan1d 9783 . . . . . . . . . . . . . . . . . . . . . . 23
158157, 152eqeltrd 2509 . . . . . . . . . . . . . . . . . . . . . 22
159 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . 23
160159eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . 22
161158, 160syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . 21
162161rexlimdva 2822 . . . . . . . . . . . . . . . . . . . 20
163150, 162syl5bi 209 . . . . . . . . . . . . . . . . . . 19
164163imp 419 . . . . . . . . . . . . . . . . . 18
165148, 164syldan 457 . . . . . . . . . . . . . . . . 17
166165adantr 452 . . . . . . . . . . . . . . . 16
167 flbi 11215 . . . . . . . . . . . . . . . 16
168112, 166, 167syl2anc 643 . . . . . . . . . . . . . . 15
169168adantr 452 . . . . . . . . . . . . . 14
170 neeq1 2606 . . . . . . . . . . . . . . . . . . . . . . . 24
171170biimparc 474 . . . . . . . . . . . . . . . . . . . . . . 23
172 iffalse 3738 . . . . . . . . . . . . . . . . . . . . . . . 24
173172necon1ai 2640 . . . . . . . . . . . . . . . . . . . . . . 23
174171, 173syl 16 . . . . . . . . . . . . . . . . . . . . . 22
175 iftrue 3737 . . . . . . . . . . . . . . . . . . . . . 22
176174, 175syl 16 . . . . . . . . . . . . . . . . . . . . 21
177 simpr 448 . . . . . . . . . . . . . . . . . . . . 21
178176, 177eqtr3d 2469 . . . . . . . . . . . . . . . . . . . 20
179178, 174eqbrtrrd 4226 . . . . . . . . . . . . . . . . . . 19
180179, 178jca 519 . . . . . . . . . . . . . . . . . 18
181180ex 424 . . . . . . . . . . . . . . . . 17
182 breq1 4207 . . . . . . . . . . . . . . . . . . . 20
183182biimparc 474 . . . . . . . . . . . . . . . . . . 19
184183, 175syl 16 . . . . . . . . . . . . . . . . . 18
185 simpr 448 . . . . . . . . . . . . . . . . . 18
186184, 185eqtrd 2467 . . . . . . . . . . . . . . . . 17
187181, 186impbid1 195 . . . . . . . . . . . . . . . 16
188187adantl 453 . . . . . . . . . . . . . . 15
189 eldifi 3461 . . . . . . . . . . . . . . . . . 18
190 nnre 9999 . . . . . . . . . . . . . . . . . . . . . . . . 25
191190ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24
19286, 191, 96syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
19313ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24
194193nn0ge0d 10269 . . . . . . . . . . . . . . . . . . . . . . 23
195 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24
196 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24
197195, 196ifboth 3762 . . . . . . . . . . . . . . . . . . . . . . 23
198192, 194, 197syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
19948, 198eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . 21
200199ralrimiva 2781 . . . . . . . . . . . . . . . . . . . 20
201 ffn 5583 . . . . . . . . . . . . . . . . . . . . . 22
20224, 201syl 16 . . . . . . . . . . . . . . . . . . . . 21
203 breq1 4207 . . . . . . . . . . . . . . . . . . . . . 22
204203ralrn 5865 . . . . . . . . . . . . . . . . . . . . 21
205202, 204syl 16 . . . . . . . . . . . . . . . . . . . 20
206200, 205mpbird 224 . . . . . . . . . . . . . . . . . . 19
207206r19.21bi 2796 . . . . . . . . . . . . . . . . . 18
208189, 207sylan2 461 . . . . . . . . . . . . . . . . 17
209208ad2antrr 707 . . . . . . . . . . . . . . . 16
210209biantrurd 495 . . . . . . . . . . . . . . 15
211137eqeq1d 2443 . . . . . . . . . . . . . . . . 17
212114recnd 9106 . . . . . . . . . . . . . . . . . 18
21333, 22sstrd 3350 . . . . . . . . . . . . . . . . . . . . . 22
214213ssdifssd 3477 . . . . . . . . . . . . . . . . . . . . 21
215214sselda 3340 . . . . . . . . . . . . . . . . . . . 20
216215adantr 452 . . . . . . . . . . . . . . . . . . 19
217216recnd 9106 . . . . . . . . . . . . . . . . . 18
218110nncnd 10008 . . . . . . . . . . . . . . . . . 18
219110nnne0d 10036 . . . . . . . . . . . . . . . . . 18
220212, 217, 218, 219divmul3d 9816 . . . . . . . . . . . . . . . . 17
221211, 220bitrd 245 . . . . . . . . . . . . . . . 16
222221adantr 452 . . . . . . . . . . . . . . 15
223188, 210, 2223bitr2d 273 . . . . . . . . . . . . . 14
224 ifnefalse 3739 . . . . . . . . . . . . . . . . . 18
225224eleq2d 2502 . . . . . . . . . . . . . . . . 17
226110nnrecred 10037 . . . . . . . . . . . . . . . . . . . . . 22
227216, 226readdcld 9107 . . . . . . . . . . . . . . . . . . . . 21
228227rexrd 9126 . . . . . . . . . . . . . . . . . . . 20
229 elioomnf 10991 . . . . . . . . . . . . . . . . . . . 20
230228, 229syl 16 . . . . . . . . . . . . . . . . . . 19
231104ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22
232 ffn 5583 . . . . . . . . . . . . . . . . . . . . . 22
233231, 232syl 16 . . . . . . . . . . . . . . . . . . . . 21
234 elpreima 5842 . . . . . . . . . . . . . . . . . . . . 21
235233, 234syl 16 . . . . . . . . . . . . . . . . . . . 20
236127biantrurd 495 . . . . . . . . . . . . . . . . . . . 20
237235, 236bitr4d 248 . . . . . . . . . . . . . . . . . . 19
238109biantrurd 495 . . . . . . . . . . . . . . . . . . 19
239230, 237, 2383bitr4d 277 . . . . . . . . . . . . . . . . . 18
240 ltmul1 9852 . . . . . . . . . . . . . . . . . . 19
241109, 227, 111, 115, 240syl112anc 1188 . . . . . . . . . . . . . . . . . 18
242226recnd 9106 . . . . . . . . . . . . . . . . . . . . 21
243217, 242, 218adddird 9105 . . . . . . . . . . . . . . . . . . . 20
244218, 219recid2d 9778 . . . . . . . . . . . . . . . . . . . . 21
245244oveq2d 6089 . . . . . . . . . . . . . . . . . . . 20
246243, 245eqtrd 2467 . . . . . . . . . . . . . . . . . . 19
247246breq2d 4216 . . . . . . . . . . . . . . . . . 18
248239, 241, 2473bitrd 271 . . . . . . . . . . . . . . . . 17
249225, 248sylan9bbr 682 . . . . . . . . . . . . . . . 16
250 lemul1 9854 . . . . . . . . . . . . . . . . . 18
251216, 109, 111, 115, 250syl112anc 1188 . . . . . . . . . . . . . . . . 17
252251adantr 452 . . . . . . . . . . . . . . . 16
253249, 252anbi12d 692 . . . . . . . . . . . . . . 15
254 ancom 438 . . . . . . . . . . . . . . 15
255253, 254syl6bb 253 . . . . . . . . . . . . . 14
256169, 223, 2553bitr4d 277 . . . . . . . . . . . . 13
257146, 256pm2.61dane 2676 . . . . . . . . . . . 12
258 eldif 3322 . . . . . . . . . . . . 13
259216rexrd 9126 . . . . . . . . . . . . . . . . . 18
260 elioomnf 10991 . . . . . . . . . . . . . . . . . 18
261259, 260syl 16 . . . . . . . . . . . . . . . . 17
262 elpreima 5842 . . . . . . . . . . . . . . . . . . 19
263233, 262syl 16 . . . . . . . . . . . . . . . . . 18
264127biantrurd 495 . . . . . . . . . . . . . . . . . 18
265263, 264bitr4d 248 . . . . . . . . . . . . . . . . 17
266109biantrurd 495 . . . . . . . . . . . . . . . . 17
267261, 265, 2663bitr4d 277 . . . . . . . . . . . . . . . 16
268267notbid 286 . . . . . . . . . . . . . . 15
269216, 109lenltd 9211 . . . . . . . . . . . . . . 15
270268, 269bitr4d 248 . . . . . . . . . . . . . 14
271270anbi2d 685 . . . . . . . . . . . . 13
272258, 271syl5bb 249 . . . . . . . . . . . 12
273257, 272bitr4d 248 . . . . . . . . . . 11
27460, 273sylan9bbr 682 . . . . . . . . . 10
275274pm5.32da 623 . . . . . . . . 9
27650, 58, 2753bitrd 271 . . . . . . . 8
277276pm5.32da 623 . . . . . . 7
27824adantr 452 . . . . . . . . 9
279278, 201syl 16 . . . . . . . 8
280 fniniseg 5843 . . . . . . . 8
281279, 280syl 16 . . . . . . 7
282 elin 3522 . . . . . . . 8
283190ad2antlr 708 . . . . . . . . . . . . . 14
284283renegcld 9456 . . . . . . . . . . . . 13
285 iccmbl 19452 . . . . . . . . . . . . 13
286284, 283, 285syl2anc 643 . . . . . . . . . . . 12
287 mblss 19419 . . . . . . . . . . . 12
288286, 287syl 16 . . . . . . . . . . 11
289288sseld 3339 . . . . . . . . . 10
290289adantrd 455 . . . . . . . . 9
291290pm4.71rd 617 . . . . . . . 8
292282, 291syl5bb 249 . . . . . . 7
293277, 281, 2923bitr4d 277 . . . . . 6
294293eqrdv 2433 . . . . 5
295 rembl 19427 . . . . . . . . 9
296 fss 5591 . . . . . . . . . . 11
2977, 67, 296sylancl 644 . . . . . . . . . 10
298 mbfima 19516 . . . . . . . . . 10 MblFn
2996, 297, 298syl2anc 643 . . . . . . . . 9
300 ifcl 3767 . . . . . . . . 9
301295, 299, 300sylancr 645 . . . . . . . 8
302 mbfima 19516 . . . . . . . . 9 MblFn
3036, 297, 302syl2anc 643 . . . . . . . 8
304 difmbl 19429 . . . . . . . 8
305301, 303, 304syl2anc 643 . . . . . . 7
306305ad2antrr 707 . . . . . 6