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

Theorem ulmdvlem3 21752
 Description: Lemma for ulmdv 21753. (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 10863 . . . . . 6
31, 2syl 16 . . . . 5
4 ulmdv.z . . . . 5
53, 4syl6eleqr 2524 . . . 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 21751 . . . . . 6
12 recnprss 21221 . . . . . . . . 9
136, 12syl 16 . . . . . . . 8
1413adantr 462 . . . . . . 7
157ffvelrnda 5831 . . . . . . . 8
16 elmapi 7222 . . . . . . . 8
1715, 16syl 16 . . . . . . 7
18 dvbsss 21219 . . . . . . . 8
1911, 18syl6eqssr 3395 . . . . . . 7
20 eqid 2433 . . . . . . 7 fldt fldt
21 eqid 2433 . . . . . . 7 fld fld
2214, 17, 19, 20, 21dvbssntr 21217 . . . . . 6 fldt
2311, 22eqsstr3d 3379 . . . . 5 fldt
2423ralrimiva 2789 . . . 4 fldt
25 biidd 237 . . . . 5 fldt fldt
2625rspcv 3058 . . . 4 fldt fldt
275, 24, 26sylc 60 . . 3 fldt
2827sselda 3344 . 2 fldt
29 ulmcl 21731 . . . . 5
3010, 29syl 16 . . . 4
3130ffvelrnda 5831 . . 3
32 rphalfcl 11003 . . . . . . . 8
3332adantl 463 . . . . . . 7
34 rphalfcl 11003 . . . . . . 7
3533, 34syl 16 . . . . . 6
36 ulmrel 21728 . . . . . . . . . 10
37 releldm 5059 . . . . . . . . . 10
3836, 10, 37sylancr 656 . . . . . . . . 9
39 ulmscl 21729 . . . . . . . . . . 11
4010, 39syl 16 . . . . . . . . . 10
41 ovex 6105 . . . . . . . . . . . . 13
4241rgenw 2773 . . . . . . . . . . . 12
43 eqid 2433 . . . . . . . . . . . . 13
4443fnmpt 5525 . . . . . . . . . . . 12
4542, 44mp1i 12 . . . . . . . . . . 11
46 ulmf2 21734 . . . . . . . . . . 11
4745, 10, 46syl2anc 654 . . . . . . . . . 10
484, 1, 40, 47ulmcau2 21746 . . . . . . . . 9
4938, 48mpbid 210 . . . . . . . 8
504uztrn2 10866 . . . . . . . . . . . . . . . . . 18
5150ad2ant2lr 740 . . . . . . . . . . . . . . . . 17
52 fveq2 5679 . . . . . . . . . . . . . . . . . . 19
5352oveq2d 6096 . . . . . . . . . . . . . . . . . 18
54 ovex 6105 . . . . . . . . . . . . . . . . . 18
5553, 43, 54fvmpt 5762 . . . . . . . . . . . . . . . . 17
5651, 55syl 16 . . . . . . . . . . . . . . . 16
5756fveq1d 5681 . . . . . . . . . . . . . . 15
58 simprr 749 . . . . . . . . . . . . . . . . . 18
594uztrn2 10866 . . . . . . . . . . . . . . . . . 18
6051, 58, 59syl2anc 654 . . . . . . . . . . . . . . . . 17
61 fveq2 5679 . . . . . . . . . . . . . . . . . . 19
6261oveq2d 6096 . . . . . . . . . . . . . . . . . 18
63 ovex 6105 . . . . . . . . . . . . . . . . . 18
6462, 43, 63fvmpt 5762 . . . . . . . . . . . . . . . . 17
6560, 64syl 16 . . . . . . . . . . . . . . . 16
6665fveq1d 5681 . . . . . . . . . . . . . . 15
6757, 66oveq12d 6098 . . . . . . . . . . . . . 14
6867fveq2d 5683 . . . . . . . . . . . . 13
6968breq1d 4290 . . . . . . . . . . . 12
7069ralbidv 2725 . . . . . . . . . . 11
71702ralbidva 2745 . . . . . . . . . 10
7271rexbidva 2722 . . . . . . . . 9
7372ralbidv 2725 . . . . . . . 8
7449, 73mpbid 210 . . . . . . 7
7574ad2antrr 718 . . . . . 6
76 breq2 4284 . . . . . . . . 9
77762ralbidv 2747 . . . . . . . 8
7877rexralbidv 2749 . . . . . . 7
7978rspcv 3058 . . . . . 6
8035, 75, 79sylc 60 . . . . 5
811ad2antrr 718 . . . . . 6
8253fveq1d 5681 . . . . . . . 8
83 eqid 2433 . . . . . . . 8
84 fvex 5689 . . . . . . . 8
8582, 83, 84fvmpt 5762 . . . . . . 7
8685adantl 463 . . . . . 6
8747ad2antrr 718 . . . . . . 7
88 simplr 747 . . . . . . 7
89 fvex 5689 . . . . . . . . . 10
904, 89eqeltri 2503 . . . . . . . . 9
9190mptex 5935 . . . . . . . 8
9291a1i 11 . . . . . . 7
9355adantl 463 . . . . . . . . 9
9493fveq1d 5681 . . . . . . . 8
9594, 86eqtr4d 2468 . . . . . . 7
9610ad2antrr 718 . . . . . . 7
974, 81, 87, 88, 92, 95, 96ulmclm 21737 . . . . . 6
984, 81, 33, 86, 97climi2 12973 . . . . 5
994rexanuz2 12821 . . . . . . 7
1004r19.2uz 12823 . . . . . . 7
10199, 100sylbir 213 . . . . . 6
10235adantr 462 . . . . . . . . . 10
103 simpllr 751 . . . . . . . . . . . . . . . 16
10487ffvelrnda 5831 . . . . . . . . . . . . . . . . . 18
10593, 104eqeltrrd 2508 . . . . . . . . . . . . . . . . 17
106 elmapi 7222 . . . . . . . . . . . . . . . . 17
107 fdm 5551 . . . . . . . . . . . . . . . . 17
108105, 106, 1073syl 20 . . . . . . . . . . . . . . . 16
109103, 108eleqtrrd 2510 . . . . . . . . . . . . . . 15
1106ad3antrrr 722 . . . . . . . . . . . . . . . 16
111 dvfg 21223 . . . . . . . . . . . . . . . 16
112 ffun 5549 . . . . . . . . . . . . . . . 16
113 funfvbrb 5804 . . . . . . . . . . . . . . . 16
114110, 111, 112, 1134syl 21 . . . . . . . . . . . . . . 15
115109, 114mpbid 210 . . . . . . . . . . . . . 14
116 eqid 2433 . . . . . . . . . . . . . . 15
117110, 12syl 16 . . . . . . . . . . . . . . 15
1187ad2antrr 718 . . . . . . . . . . . . . . . . 17
119118ffvelrnda 5831 . . . . . . . . . . . . . . . 16
120 elmapi 7222 . . . . . . . . . . . . . . . 16
121119, 120syl 16 . . . . . . . . . . . . . . 15
12219ralrimiva 2789 . . . . . . . . . . . . . . . . 17
123 biidd 237 . . . . . . . . . . . . . . . . . 18
124123rspcv 3058 . . . . . . . . . . . . . . . . 17
1255, 122, 124sylc 60 . . . . . . . . . . . . . . . 16
126125ad3antrrr 722 . . . . . . . . . . . . . . 15
12720, 21, 116, 117, 121, 126eldv 21215 . . . . . . . . . . . . . 14 fldt lim
128115, 127mpbid 210 . . . . . . . . . . . . 13 fldt lim
129128simprd 460 . . . . . . . . . . . 12 lim
130125adantr 462 . . . . . . . . . . . . . . . . 17
13113adantr 462 . . . . . . . . . . . . . . . . 17
132130, 131sstrd 3354 . . . . . . . . . . . . . . . 16
133132ad2antrr 718 . . . . . . . . . . . . . . 15
134121, 133, 103dvlem 21213 . . . . . . . . . . . . . 14
135134, 116fmptd 5855 . . . . . . . . . . . . 13
136133ssdifssd 3482 . . . . . . . . . . . . 13
137133, 103sseldd 3345 . . . . . . . . . . . . 13
138135, 136, 137ellimc3 21196 . . . . . . . . . . . 12 lim
139129, 138mpbid 210 . . . . . . . . . . 11
140139simprd 460 . . . . . . . . . 10
141 fveq2 5679 . . . . . . . . . . . . . . . . . . . 20
142141oveq1d 6095 . . . . . . . . . . . . . . . . . . 19
143 oveq1 6087 . . . . . . . . . . . . . . . . . . 19
144142, 143oveq12d 6098 . . . . . . . . . . . . . . . . . 18
145 ovex 6105 . . . . . . . . . . . . . . . . . 18
146144, 116, 145fvmpt 5762 . . . . . . . . . . . . . . . . 17
147146oveq1d 6095 . . . . . . . . . . . . . . . 16
148147fveq2d 5683 . . . . . . . . . . . . . . 15
149 id 22 . . . . . . . . . . . . . . 15
150148, 149breqan12rd 4296 . . . . . . . . . . . . . 14
151150imbi2d 316 . . . . . . . . . . . . 13
152151ralbidva 2721 . . . . . . . . . . . 12
153152rexbidv 2726 . . . . . . . . . . 11
154153rspcv 3058 . . . . . . . . . 10
155102, 140, 154sylc 60 . . . . . . . . 9
156155adantrr 709 . . . . . . . 8
157 cnxmet 20194 . . . . . . . . . . . 12
158 xmetres2 19778 . . . . . . . . . . . 12
159157, 131, 158sylancr 656 . . . . . . . . . . 11
160159ad3antrrr 722 . . . . . . . . . 10
16121cnfldtop 20205 . . . . . . . . . . . . . . . . 17 fld
162 resttop 18606 . . . . . . . . . . . . . . . . 17 fld fldt
163161, 6, 162sylancr 656 . . . . . . . . . . . . . . . 16 fldt
16421cnfldtopon 20204 . . . . . . . . . . . . . . . . . . 19 fld TopOn
165 resttopon 18607 . . . . . . . . . . . . . . . . . . 19 fld TopOn fldt TopOn
166164, 13, 165sylancr 656 . . . . . . . . . . . . . . . . . 18 fldt TopOn
167 toponuni 18374 . . . . . . . . . . . . . . . . . 18 fldt TopOn fldt
168166, 167syl 16 . . . . . . . . . . . . . . . . 17 fldt
169125, 168sseqtrd 3380 . . . . . . . . . . . . . . . 16 fldt
170 eqid 2433 . . . . . . . . . . . . . . . . 17 fldt fldt
171170ntrss2 18503 . . . . . . . . . . . . . . . 16 fldt fldt fldt
172163, 169, 171syl2anc 654 . . . . . . . . . . . . . . 15 fldt
173172, 27eqssd 3361 . . . . . . . . . . . . . 14 fldt
174170isopn3 18512 . . . . . . . . . . . . . . 15 fldt fldt fldt fldt
175163, 169, 174syl2anc 654 . . . . . . . . . . . . . 14 fldt fldt
176173, 175mpbird 232 . . . . . . . . . . . . 13 fldt
177 eqid 2433 . . . . . . . . . . . . . . 15
17821cnfldtopn 20203 . . . . . . . . . . . . . . 15 fld
179 eqid 2433 . . . . . . . . . . . . . . 15
180177, 178, 179metrest 19941 . . . . . . . . . . . . . 14 fldt
181157, 13, 180sylancr 656 . . . . . . . . . . . . 13 fldt
182176, 181eleqtrd 2509 . . . . . . . . . . . 12
183182adantr 462 . . . . . . . . . . 11
184183ad3antrrr 722 . . . . . . . . . 10
18588ad2antrr 718 . . . . . . . . . 10
186 simprl 748 . . . . . . . . . 10
187179mopni3 19911 . . . . . . . . . 10
188160, 184, 185, 186, 187syl31anc 1214 . . . . . . . . 9
189 anass 642 . . . . . . . . . . . . . . . . . 18
190 df-3an 960 . . . . . . . . . . . . . . . . . . . . 21
191 anass 642 . . . . . . . . . . . . . . . . . . . . . 22
1929ralrimiva 2789 . . . . . . . . . . . . . . . . . . . . . . . . 25
193 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
194193mpteq2dv 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
195 fveq2 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
196194, 195breq12d 4293 . . . . . . . . . . . . . . . . . . . . . . . . . 26
197196rspccva 3061 . . . . . . . . . . . . . . . . . . . . . . . . 25
198192, 197sylan 468 . . . . . . . . . . . . . . . . . . . . . . . 24
199 simprll 754 . . . . . . . . . . . . . . . . . . . . . . . 24
200 simprlr 755 . . . . . . . . . . . . . . . . . . . . . . . 24
201 simprr3 1031 . . . . . . . . . . . . . . . . . . . . . . . . 25
202 simplll 750 . . . . . . . . . . . . . . . . . . . . . . . . 25
203201, 202syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
204 simplr 747 . . . . . . . . . . . . . . . . . . . . . . . . 25
205201, 204syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
206 simpllr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26
207201, 206syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
208207simpld 456 . . . . . . . . . . . . . . . . . . . . . . . 24
209207simprd 460 . . . . . . . . . . . . . . . . . . . . . . . 24
210 simpr3 989 . . . . . . . . . . . . . . . . . . . . . . . . . 26
211201, 210syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
212211simprd 460 . . . . . . . . . . . . . . . . . . . . . . . 24
213 simprr1 1029 . . . . . . . . . . . . . . . . . . . . . . . 24
214 simprr2 1030 . . . . . . . . . . . . . . . . . . . . . . . . 25
215214simpld 456 . . . . . . . . . . . . . . . . . . . . . . . 24
216214simprd 460 . . . . . . . . . . . . . . . . . . . . . . . 24
217 simpr1 987 . . . . . . . . . . . . . . . . . . . . . . . . . 26