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

Theorem ulmdvlem3 23436
 Description: Lemma for ulmdv 23437. (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 11197 . . . . . 6
31, 2syl 17 . . . . 5
4 ulmdv.z . . . . 5
53, 4syl6eleqr 2560 . . . 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 23435 . . . . . 6
12 recnprss 22938 . . . . . . . . 9
136, 12syl 17 . . . . . . . 8
1413adantr 472 . . . . . . 7
157ffvelrnda 6037 . . . . . . . 8
16 elmapi 7511 . . . . . . . 8
1715, 16syl 17 . . . . . . 7
18 dvbsss 22936 . . . . . . . 8
1911, 18syl6eqssr 3469 . . . . . . 7
20 eqid 2471 . . . . . . 7 fldt fldt
21 eqid 2471 . . . . . . 7 fld fld
2214, 17, 19, 20, 21dvbssntr 22934 . . . . . 6 fldt
2311, 22eqsstr3d 3453 . . . . 5 fldt
2423ralrimiva 2809 . . . 4 fldt
25 biidd 245 . . . . 5 fldt fldt
2625rspcv 3132 . . . 4 fldt fldt
275, 24, 26sylc 61 . . 3 fldt
2827sselda 3418 . 2 fldt
29 ulmcl 23415 . . . . 5
3010, 29syl 17 . . . 4
3130ffvelrnda 6037 . . 3
32 rphalfcl 11350 . . . . . . . 8
3332adantl 473 . . . . . . 7
34 rphalfcl 11350 . . . . . . 7
3533, 34syl 17 . . . . . 6
36 ulmrel 23412 . . . . . . . . . 10
37 releldm 5073 . . . . . . . . . 10
3836, 10, 37sylancr 676 . . . . . . . . 9
39 ulmscl 23413 . . . . . . . . . . 11
4010, 39syl 17 . . . . . . . . . 10
41 ovex 6336 . . . . . . . . . . . . 13
4241rgenw 2768 . . . . . . . . . . . 12
43 eqid 2471 . . . . . . . . . . . . 13
4443fnmpt 5714 . . . . . . . . . . . 12
4542, 44mp1i 13 . . . . . . . . . . 11
46 ulmf2 23418 . . . . . . . . . . 11
4745, 10, 46syl2anc 673 . . . . . . . . . 10
484, 1, 40, 47ulmcau2 23430 . . . . . . . . 9
4938, 48mpbid 215 . . . . . . . 8
504uztrn2 11200 . . . . . . . . . . . . . . . . . 18
5150ad2ant2lr 762 . . . . . . . . . . . . . . . . 17
52 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
5352oveq2d 6324 . . . . . . . . . . . . . . . . . 18
54 ovex 6336 . . . . . . . . . . . . . . . . . 18
5553, 43, 54fvmpt 5963 . . . . . . . . . . . . . . . . 17
5651, 55syl 17 . . . . . . . . . . . . . . . 16
5756fveq1d 5881 . . . . . . . . . . . . . . 15
58 simprr 774 . . . . . . . . . . . . . . . . . 18
594uztrn2 11200 . . . . . . . . . . . . . . . . . 18
6051, 58, 59syl2anc 673 . . . . . . . . . . . . . . . . 17
61 fveq2 5879 . . . . . . . . . . . . . . . . . . 19
6261oveq2d 6324 . . . . . . . . . . . . . . . . . 18
63 ovex 6336 . . . . . . . . . . . . . . . . . 18
6462, 43, 63fvmpt 5963 . . . . . . . . . . . . . . . . 17
6560, 64syl 17 . . . . . . . . . . . . . . . 16
6665fveq1d 5881 . . . . . . . . . . . . . . 15
6757, 66oveq12d 6326 . . . . . . . . . . . . . 14
6867fveq2d 5883 . . . . . . . . . . . . 13
6968breq1d 4405 . . . . . . . . . . . 12
7069ralbidv 2829 . . . . . . . . . . 11
71702ralbidva 2831 . . . . . . . . . 10
7271rexbidva 2889 . . . . . . . . 9
7372ralbidv 2829 . . . . . . . 8
7449, 73mpbid 215 . . . . . . 7
7574ad2antrr 740 . . . . . 6
76 breq2 4399 . . . . . . . . 9
77762ralbidv 2832 . . . . . . . 8
7877rexralbidv 2898 . . . . . . 7
7978rspcv 3132 . . . . . 6
8035, 75, 79sylc 61 . . . . 5
811ad2antrr 740 . . . . . 6
8253fveq1d 5881 . . . . . . . 8
83 eqid 2471 . . . . . . . 8
84 fvex 5889 . . . . . . . 8
8582, 83, 84fvmpt 5963 . . . . . . 7
8685adantl 473 . . . . . 6
8747ad2antrr 740 . . . . . . 7
88 simplr 770 . . . . . . 7
89 fvex 5889 . . . . . . . . . 10
904, 89eqeltri 2545 . . . . . . . . 9
9190mptex 6152 . . . . . . . 8
9291a1i 11 . . . . . . 7
9355adantl 473 . . . . . . . . 9
9493fveq1d 5881 . . . . . . . 8
9594, 86eqtr4d 2508 . . . . . . 7
9610ad2antrr 740 . . . . . . 7
974, 81, 87, 88, 92, 95, 96ulmclm 23421 . . . . . 6
984, 81, 33, 86, 97climi2 13652 . . . . 5
994rexanuz2 13489 . . . . . . 7
1004r19.2uz 13491 . . . . . . 7
10199, 100sylbir 218 . . . . . 6
10235adantr 472 . . . . . . . . . 10
103 simpllr 777 . . . . . . . . . . . . . . . 16
10487ffvelrnda 6037 . . . . . . . . . . . . . . . . . 18
10593, 104eqeltrrd 2550 . . . . . . . . . . . . . . . . 17
106 elmapi 7511 . . . . . . . . . . . . . . . . 17
107 fdm 5745 . . . . . . . . . . . . . . . . 17
108105, 106, 1073syl 18 . . . . . . . . . . . . . . . 16
109103, 108eleqtrrd 2552 . . . . . . . . . . . . . . 15
1106ad3antrrr 744 . . . . . . . . . . . . . . . 16
111 dvfg 22940 . . . . . . . . . . . . . . . 16
112 ffun 5742 . . . . . . . . . . . . . . . 16
113 funfvbrb 6010 . . . . . . . . . . . . . . . 16
114110, 111, 112, 1134syl 19 . . . . . . . . . . . . . . 15
115109, 114mpbid 215 . . . . . . . . . . . . . 14
116 eqid 2471 . . . . . . . . . . . . . . 15
117110, 12syl 17 . . . . . . . . . . . . . . 15
1187ad2antrr 740 . . . . . . . . . . . . . . . . 17
119118ffvelrnda 6037 . . . . . . . . . . . . . . . 16
120 elmapi 7511 . . . . . . . . . . . . . . . 16
121119, 120syl 17 . . . . . . . . . . . . . . 15
12219ralrimiva 2809 . . . . . . . . . . . . . . . . 17
123 biidd 245 . . . . . . . . . . . . . . . . . 18
124123rspcv 3132 . . . . . . . . . . . . . . . . 17
1255, 122, 124sylc 61 . . . . . . . . . . . . . . . 16
126125ad3antrrr 744 . . . . . . . . . . . . . . 15
12720, 21, 116, 117, 121, 126eldv 22932 . . . . . . . . . . . . . 14 fldt lim
128115, 127mpbid 215 . . . . . . . . . . . . 13 fldt lim
129128simprd 470 . . . . . . . . . . . 12 lim
130125adantr 472 . . . . . . . . . . . . . . . . 17
13113adantr 472 . . . . . . . . . . . . . . . . 17
132130, 131sstrd 3428 . . . . . . . . . . . . . . . 16
133132ad2antrr 740 . . . . . . . . . . . . . . 15
134121, 133, 103dvlem 22930 . . . . . . . . . . . . . 14
135134, 116fmptd 6061 . . . . . . . . . . . . 13
136133ssdifssd 3560 . . . . . . . . . . . . 13
137133, 103sseldd 3419 . . . . . . . . . . . . 13
138135, 136, 137ellimc3 22913 . . . . . . . . . . . 12 lim
139129, 138mpbid 215 . . . . . . . . . . 11
140139simprd 470 . . . . . . . . . 10
141 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20
142141oveq1d 6323 . . . . . . . . . . . . . . . . . . 19
143 oveq1 6315 . . . . . . . . . . . . . . . . . . 19
144142, 143oveq12d 6326 . . . . . . . . . . . . . . . . . 18
145 ovex 6336 . . . . . . . . . . . . . . . . . 18
146144, 116, 145fvmpt 5963 . . . . . . . . . . . . . . . . 17
147146oveq1d 6323 . . . . . . . . . . . . . . . 16
148147fveq2d 5883 . . . . . . . . . . . . . . 15
149 id 22 . . . . . . . . . . . . . . 15
150148, 149breqan12rd 4412 . . . . . . . . . . . . . 14
151150imbi2d 323 . . . . . . . . . . . . 13
152151ralbidva 2828 . . . . . . . . . . . 12
153152rexbidv 2892 . . . . . . . . . . 11
154153rspcv 3132 . . . . . . . . . 10
155102, 140, 154sylc 61 . . . . . . . . 9
156155adantrr 731 . . . . . . . 8
157 anass 661 . . . . . . . . . . . . . . . 16
158 df-3an 1009 . . . . . . . . . . . . . . . . . . 19
159 anass 661 . . . . . . . . . . . . . . . . . . . 20
1609ralrimiva 2809 . . . . . . . . . . . . . . . . . . . . . . 23
161 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . 26
162161mpteq2dv 4483 . . . . . . . . . . . . . . . . . . . . . . . . 25
163 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
164162, 163breq12d 4408 . . . . . . . . . . . . . . . . . . . . . . . 24
165164rspccva 3135 . . . . . . . . . . . . . . . . . . . . . . 23
166160, 165sylan 479 . . . . . . . . . . . . . . . . . . . . . 22
167 simprll 780 . . . . . . . . . . . . . . . . . . . . . 22
168 simprlr 781 . . . . . . . . . . . . . . . . . . . . . 22
169 simprr3 1080 . . . . . . . . . . . . . . . . . . . . . . 23
170 simplll 776 . . . . . . . . . . . . . . . . . . . . . . 23
171169, 170syl 17 . . . . . . . . . . . . . . . . . . . . . 22
172 simplr 770 . . . . . . . . . . . . . . . . . . . . . . 23
173169, 172syl 17 . . . . . . . . . . . . . . . . . . . . . 22
174 simpllr 777 . . . . . . . . . . . . . . . . . . . . . . . 24
175169, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
176175simpld 466 . . . . . . . . . . . . . . . . . . . . . 22
177175simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
178 simpr3 1038 . . . . . . . . . . . . . . . . . . . . . . . 24
179169, 178syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
180179simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
181 simprr1 1078 . . . . . . . . . . . . . . . . . . . . . 22
182 simprr2 1079 . . . . . . . . . . . . . . . . . . . . . . 23
183182simpld 466 . . . . . . . . . . . . . . . . . . . . . 22
184182simprd 470 . . . . . . . . . . . . . . . . . . . . . 22
185 simpr1 1036 . . . . . . . . . . . . . . . . . . . . . . . 24
186169, 185syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
187186eldifad 3402 . . . . . . . . . . . . . . . . . . . . . 22
188179simpld 466 . . . . . . . . . . . . . . . . . . . . . 22
189 simpr2 1037 . . . . . . . . . . . . . . . . . . . . . . . 24
190169, 189syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
191188, 190mpand 689 . . . . . . . . . . . . . . . . . . . . . 22
1924, 6, 1, 7, 8, 166, 10, 167, 168, 171, 173, 176, 177, 180, 181, 183, 184, 187, 188, 191ulmdvlem1 23434 . . . . . . . . . . . . . . . . . . . . 21