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

Theorem ulmdvlem3 19795
 Description: Lemma for ulmdv 19796. (Contributed by Mario Carneiro, 8-May-2015.) (Proof shortened by Mario Carneiro, 28-Dec-2016.)
Hypotheses
Ref Expression
ulmdv.z
ulmdv.s
ulmdv.m
ulmdv.f
ulmdv.g
ulmdv.l
ulmdv.u
Assertion
Ref Expression
ulmdvlem3
Distinct variable groups:   ,,   ,   ,   ,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ulmdvlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ulmdv.m . . . . . 6
2 uzid 10258 . . . . . 6
31, 2syl 15 . . . . 5
4 ulmdv.z . . . . 5
53, 4syl6eleqr 2387 . . . 4
6 ulmdv.s . . . . . . 7
7 ulmdv.f . . . . . . 7
8 ulmdv.g . . . . . . 7
9 ulmdv.l . . . . . . 7
10 ulmdv.u . . . . . . 7
114, 6, 1, 7, 8, 9, 10ulmdvlem2 19794 . . . . . 6
12 recnprss 19270 . . . . . . . . 9
136, 12syl 15 . . . . . . . 8
1413adantr 451 . . . . . . 7
15 ffvelrn 5679 . . . . . . . . 9
167, 15sylan 457 . . . . . . . 8
17 elmapi 6808 . . . . . . . 8
1816, 17syl 15 . . . . . . 7
19 dvbsss 19268 . . . . . . . . 9
2019a1i 10 . . . . . . . 8
2111, 20eqsstr3d 3226 . . . . . . 7
22 eqid 2296 . . . . . . 7 fldt fldt
23 eqid 2296 . . . . . . 7 fld fld
2414, 18, 21, 22, 23dvbssntr 19266 . . . . . 6 fldt
2511, 24eqsstr3d 3226 . . . . 5 fldt
2625ralrimiva 2639 . . . 4 fldt
27 biidd 228 . . . . 5 fldt fldt
2827rspcv 2893 . . . 4 fldt fldt
295, 26, 28sylc 56 . . 3 fldt
3029sselda 3193 . 2 fldt
31 ulmcl 19776 . . . . 5
3210, 31syl 15 . . . 4
33 ffvelrn 5679 . . . 4
3432, 33sylan 457 . . 3
35 rphalfcl 10394 . . . . . . . 8
3635adantl 452 . . . . . . 7
37 rphalfcl 10394 . . . . . . 7
3836, 37syl 15 . . . . . 6
39 ulmrel 19773 . . . . . . . . . 10
40 releldm 4927 . . . . . . . . . 10
4139, 10, 40sylancr 644 . . . . . . . . 9
42 ulmscl 19774 . . . . . . . . . . 11
4310, 42syl 15 . . . . . . . . . 10
44 ovex 5899 . . . . . . . . . . . . 13
4544rgenw 2623 . . . . . . . . . . . 12
46 eqid 2296 . . . . . . . . . . . . 13
4746fnmpt 5386 . . . . . . . . . . . 12
4845, 47mp1i 11 . . . . . . . . . . 11
49 ulmf2 19779 . . . . . . . . . . 11
5048, 10, 49syl2anc 642 . . . . . . . . . 10
514, 1, 43, 50ulmcau2 19789 . . . . . . . . 9
5241, 51mpbid 201 . . . . . . . 8
534uztrn2 10261 . . . . . . . . . . . . . . . . . 18
5453ad2ant2lr 728 . . . . . . . . . . . . . . . . 17
55 fveq2 5541 . . . . . . . . . . . . . . . . . . 19
5655oveq2d 5890 . . . . . . . . . . . . . . . . . 18
57 ovex 5899 . . . . . . . . . . . . . . . . . 18
5856, 46, 57fvmpt 5618 . . . . . . . . . . . . . . . . 17
5954, 58syl 15 . . . . . . . . . . . . . . . 16
6059fveq1d 5543 . . . . . . . . . . . . . . 15
61 simprr 733 . . . . . . . . . . . . . . . . . 18
624uztrn2 10261 . . . . . . . . . . . . . . . . . 18
6354, 61, 62syl2anc 642 . . . . . . . . . . . . . . . . 17
64 fveq2 5541 . . . . . . . . . . . . . . . . . . 19
6564oveq2d 5890 . . . . . . . . . . . . . . . . . 18
66 ovex 5899 . . . . . . . . . . . . . . . . . 18
6765, 46, 66fvmpt 5618 . . . . . . . . . . . . . . . . 17
6863, 67syl 15 . . . . . . . . . . . . . . . 16
6968fveq1d 5543 . . . . . . . . . . . . . . 15
7060, 69oveq12d 5892 . . . . . . . . . . . . . 14
7170fveq2d 5545 . . . . . . . . . . . . 13
7271breq1d 4049 . . . . . . . . . . . 12
7372ralbidv 2576 . . . . . . . . . . 11
74732ralbidva 2596 . . . . . . . . . 10
7574rexbidva 2573 . . . . . . . . 9
7675ralbidv 2576 . . . . . . . 8
7752, 76mpbid 201 . . . . . . 7
7877ad2antrr 706 . . . . . 6
79 breq2 4043 . . . . . . . . 9
80792ralbidv 2598 . . . . . . . 8
8180rexralbidv 2600 . . . . . . 7
8281rspcv 2893 . . . . . 6
8338, 78, 82sylc 56 . . . . 5
841ad2antrr 706 . . . . . 6
8556fveq1d 5543 . . . . . . . 8
86 eqid 2296 . . . . . . . 8
87 fvex 5555 . . . . . . . 8
8885, 86, 87fvmpt 5618 . . . . . . 7
8988adantl 452 . . . . . 6
9050ad2antrr 706 . . . . . . 7
91 simplr 731 . . . . . . 7
92 fvex 5555 . . . . . . . . . 10
934, 92eqeltri 2366 . . . . . . . . 9
9493mptex 5762 . . . . . . . 8
9594a1i 10 . . . . . . 7
9658adantl 452 . . . . . . . . 9
9796fveq1d 5543 . . . . . . . 8
9897, 89eqtr4d 2331 . . . . . . 7
9910ad2antrr 706 . . . . . . 7
1004, 84, 90, 91, 95, 98, 99ulmclm 19782 . . . . . 6
1014, 84, 36, 89, 100climi2 12001 . . . . 5
1024rexanuz2 11849 . . . . . . 7
1034r19.2uz 11851 . . . . . . 7
104102, 103sylbir 204 . . . . . 6
10538adantr 451 . . . . . . . . . . 11
106 simpllr 735 . . . . . . . . . . . . . . . . 17
107 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . 21
10890, 107sylan 457 . . . . . . . . . . . . . . . . . . . 20
10996, 108eqeltrrd 2371 . . . . . . . . . . . . . . . . . . 19
110 elmapi 6808 . . . . . . . . . . . . . . . . . . 19
111109, 110syl 15 . . . . . . . . . . . . . . . . . 18
112 fdm 5409 . . . . . . . . . . . . . . . . . 18
113111, 112syl 15 . . . . . . . . . . . . . . . . 17
114106, 113eleqtrrd 2373 . . . . . . . . . . . . . . . 16
1156ad3antrrr 710 . . . . . . . . . . . . . . . . . 18
116 dvfg 19272 . . . . . . . . . . . . . . . . . 18
117115, 116syl 15 . . . . . . . . . . . . . . . . 17
118 ffun 5407 . . . . . . . . . . . . . . . . 17
119 funfvbrb 5654 . . . . . . . . . . . . . . . . 17
120117, 118, 1193syl 18 . . . . . . . . . . . . . . . 16
121114, 120mpbid 201 . . . . . . . . . . . . . . 15
122 eqid 2296 . . . . . . . . . . . . . . . 16
123115, 12syl 15 . . . . . . . . . . . . . . . 16
1247ad2antrr 706 . . . . . . . . . . . . . . . . . 18
125 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18
126124, 125sylan 457 . . . . . . . . . . . . . . . . 17
127 elmapi 6808 . . . . . . . . . . . . . . . . 17
128126, 127syl 15 . . . . . . . . . . . . . . . 16
12921ralrimiva 2639 . . . . . . . . . . . . . . . . . 18
130 biidd 228 . . . . . . . . . . . . . . . . . . 19
131130rspcv 2893 . . . . . . . . . . . . . . . . . 18
1325, 129, 131sylc 56 . . . . . . . . . . . . . . . . 17
133132ad3antrrr 710 . . . . . . . . . . . . . . . 16
13422, 23, 122, 123, 128, 133eldv 19264 . . . . . . . . . . . . . . 15 fldt lim
135121, 134mpbid 201 . . . . . . . . . . . . . 14 fldt lim
136135simprd 449 . . . . . . . . . . . . 13 lim
137132adantr 451 . . . . . . . . . . . . . . . . . 18
13813adantr 451 . . . . . . . . . . . . . . . . . 18
139137, 138sstrd 3202 . . . . . . . . . . . . . . . . 17
140139ad2antrr 706 . . . . . . . . . . . . . . . 16
141128, 140, 106dvlem 19262 . . . . . . . . . . . . . . 15
142141, 122fmptd 5700 . . . . . . . . . . . . . 14
143 difss 3316 . . . . . . . . . . . . . . 15
144143, 140syl5ss 3203 . . . . . . . . . . . . . 14
145140, 106sseldd 3194 . . . . . . . . . . . . . 14
146142, 144, 145ellimc3 19245 . . . . . . . . . . . . 13 lim
147136, 146mpbid 201 . . . . . . . . . . . 12
148147simprd 449 . . . . . . . . . . 11
149 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21
150149oveq1d 5889 . . . . . . . . . . . . . . . . . . . 20
151 oveq1 5881 . . . . . . . . . . . . . . . . . . . 20
152150, 151oveq12d 5892 . . . . . . . . . . . . . . . . . . 19
153 ovex 5899 . . . . . . . . . . . . . . . . . . 19
154152, 122, 153fvmpt 5618 . . . . . . . . . . . . . . . . . 18
155154oveq1d 5889 . . . . . . . . . . . . . . . . 17
156155fveq2d 5545 . . . . . . . . . . . . . . . 16
157 id 19 . . . . . . . . . . . . . . . 16
158156, 157breqan12rd 4055 . . . . . . . . . . . . . . 15
159158imbi2d 307 . . . . . . . . . . . . . 14
160159ralbidva 2572 . . . . . . . . . . . . 13
161160rexbidv 2577 . . . . . . . . . . . 12
162161rspcv 2893 . . . . . . . . . . 11
163105, 148, 162sylc 56 . . . . . . . . . 10
164163adantrr 697 . . . . . . . . 9
165 cnxmet 18298 . . . . . . . . . . . . . . 15
166 xmetres2 17941 . . . . . . . . . . . . . . 15
167165, 138, 166sylancr 644 . . . . . . . . . . . . . 14
168167ad3antrrr 710 . . . . . . . . . . . . 13
16923cnfldtop 18309 . . . . . . . . . . . . . . . . . . . 20 fld
170 resttop 16907 . . . . . . . . . . . . . . . . . . . 20 fld fldt
171169, 6, 170sylancr 644 . . . . . . . . . . . . . . . . . . 19 fldt
17223cnfldtopon 18308 . . . . . . . . . . . . . . . . . . . . . 22 fld TopOn
173 resttopon 16908 . . . . . . . . . . . . . . . . . . . . . 22 fld TopOn fldt TopOn
174172, 13, 173sylancr 644 . . . . . . . . . . . . . . . . . . . . 21 fldt TopOn
175 toponuni 16681 . . . . . . . . . . . . . . . . . . . . 21 fldt TopOn fldt
176174, 175syl 15 . . . . . . . . . . . . . . . . . . . 20 fldt
177132, 176sseqtrd 3227 . . . . . . . . . . . . . . . . . . 19 fldt
178 eqid 2296 . . . . . . . . . . . . . . . . . . . 20 fldt fldt
179178ntrss2 16810 . . . . . . . . . . . . . . . . . . 19 fldt fldt fldt
180171, 177, 179syl2anc 642 . . . . . . . . . . . . . . . . . 18 fldt
181180, 29eqssd 3209 . . . . . . . . . . . . . . . . 17 fldt
182178isopn3 16819 . . . . . . . . . . . . . . . . . 18 fldt fldt fldt fldt
183171, 177, 182syl2anc 642 . . . . . . . . . . . . . . . . 17 fldt fldt
184181, 183mpbird 223 . . . . . . . . . . . . . . . 16 fldt
185 eqid 2296 . . . . . . . . . . . . . . . . . 18
18623cnfldtopn 18307 . . . . . . . . . . . . . . . . . 18 fld
187 eqid 2296 . . . . . . . . . . . . . . . . . 18
188185, 186, 187metrest 18086 . . . . . . . . . . . . . . . . 17 fldt
189165, 13, 188sylancr 644 . . . . . . . . . . . . . . . 16 fldt
190184, 189eleqtrd 2372 . . . . . . . . . . . . . . 15
191190adantr 451 . . . . . . . . . . . . . 14
192191ad3antrrr 710 . . . . . . . . . . . . 13
19391ad2antrr 706 . . . . . . . . . . . . 13
194 simprl 732 . . . . . . . . . . . . 13
195187mopni3 18056 . . . . . . . . . . . . 13
196168, 192, 193, 194, 195syl31anc 1185 . . . . . . . . . . . 12
197 anass 630 . . . . . . . . . . . . . . . . . . . . 21
198 df-3an 936 . . . . . . . . . . . . . . . . . . . . . . . 24
199 anass 630 . . . . . . . . . . . . . . . . . . . . . . . . 25
2009ralrimiva 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
202201mpteq2dv 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
203 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
204202, 203breq12d 4052 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
205204rspccva 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
206200, 205sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
207 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
208 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
209 simprr3 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
210 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
211209, 210syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
212 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
213209, 212syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
214 simpllr 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
215209, 214syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
216215simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
217215simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
218 simpr3 963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
219209, 218syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
220219simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
221 simprr1 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
222 simprr2 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
223222simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
224222simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27