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

Theorem ulmcau 20311
 Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every there is a such that for all the functions and are uniformly within of each other on . This is the four-quantifier version, see ulmcau2 20312 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015.)
Hypotheses
Ref Expression
ulmcau.z
ulmcau.m
ulmcau.s
ulmcau.f
Assertion
Ref Expression
ulmcau
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,
Allowed substitution hints:   ()   (,,,)

Proof of Theorem ulmcau
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldmg 5065 . . . 4
21ibi 233 . . 3
3 ulmcau.z . . . . . . . 8
4 ulmcau.m . . . . . . . . 9
54ad2antrr 707 . . . . . . . 8
6 ulmcau.f . . . . . . . . 9
76ad2antrr 707 . . . . . . . 8
8 eqidd 2437 . . . . . . . 8
9 eqidd 2437 . . . . . . . 8
10 simplr 732 . . . . . . . 8
11 rphalfcl 10636 . . . . . . . . 9
1211adantl 453 . . . . . . . 8
133, 5, 7, 8, 9, 10, 12ulmi 20302 . . . . . . 7
14 simpr 448 . . . . . . . . . . . 12
1514, 3syl6eleq 2526 . . . . . . . . . . 11
16 eluzelz 10496 . . . . . . . . . . 11
17 uzid 10500 . . . . . . . . . . 11
1815, 16, 173syl 19 . . . . . . . . . 10
19 fveq2 5728 . . . . . . . . . . . . . . . 16
2019fveq1d 5730 . . . . . . . . . . . . . . 15
2120oveq1d 6096 . . . . . . . . . . . . . 14
2221fveq2d 5732 . . . . . . . . . . . . 13
2322breq1d 4222 . . . . . . . . . . . 12
2423ralbidv 2725 . . . . . . . . . . 11
2524rspcv 3048 . . . . . . . . . 10
2618, 25syl 16 . . . . . . . . 9
27 r19.26 2838 . . . . . . . . . . . . . . 15
287ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . 24
2928adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
30 elmapi 7038 . . . . . . . . . . . . . . . . . . . . . . 23
3129, 30syl 16 . . . . . . . . . . . . . . . . . . . . . 22
3231ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . 21
33 ulmcl 20297 . . . . . . . . . . . . . . . . . . . . . . 23
3433ad4antlr 714 . . . . . . . . . . . . . . . . . . . . . 22
3534ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . 21
3632, 35abssubd 12255 . . . . . . . . . . . . . . . . . . . 20
3736breq1d 4222 . . . . . . . . . . . . . . . . . . 19
3837biimpd 199 . . . . . . . . . . . . . . . . . 18
393uztrn2 10503 . . . . . . . . . . . . . . . . . . . . . . 23
40 ffvelrn 5868 . . . . . . . . . . . . . . . . . . . . . . 23
417, 39, 40syl2an 464 . . . . . . . . . . . . . . . . . . . . . 22
4241anassrs 630 . . . . . . . . . . . . . . . . . . . . 21
43 elmapi 7038 . . . . . . . . . . . . . . . . . . . . 21
4442, 43syl 16 . . . . . . . . . . . . . . . . . . . 20
4544ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19
46 rpre 10618 . . . . . . . . . . . . . . . . . . . 20
4746ad4antlr 714 . . . . . . . . . . . . . . . . . . 19
48 abs3lem 12142 . . . . . . . . . . . . . . . . . . 19
4945, 32, 35, 47, 48syl22anc 1185 . . . . . . . . . . . . . . . . . 18
5038, 49sylan2d 469 . . . . . . . . . . . . . . . . 17
5150ancomsd 441 . . . . . . . . . . . . . . . 16
5251ralimdva 2784 . . . . . . . . . . . . . . 15
5327, 52syl5bir 210 . . . . . . . . . . . . . 14
5453expdimp 427 . . . . . . . . . . . . 13
5554an32s 780 . . . . . . . . . . . 12
5655ralimdva 2784 . . . . . . . . . . 11
5756ex 424 . . . . . . . . . 10
5857com23 74 . . . . . . . . 9
5926, 58mpdd 38 . . . . . . . 8
6059reximdva 2818 . . . . . . 7
6113, 60mpd 15 . . . . . 6
6261ralrimiva 2789 . . . . 5
6362ex 424 . . . 4
6463exlimdv 1646 . . 3
652, 64syl5 30 . 2
66 ulmrel 20294 . . . 4
67 ulmcau.s . . . . . . . . . 10
683, 4, 67, 6ulmcaulem 20310 . . . . . . . . 9
6968biimpa 471 . . . . . . . 8
70 rphalfcl 10636 . . . . . . . 8
71 breq2 4216 . . . . . . . . . . . . 13
7271ralbidv 2725 . . . . . . . . . . . 12
73722ralbidv 2747 . . . . . . . . . . 11
7473rexbidv 2726 . . . . . . . . . 10
75 ralcom 2868 . . . . . . . . . . . . . 14
76 fveq2 5728 . . . . . . . . . . . . . . 15
77 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20
78 fveq2 5728 . . . . . . . . . . . . . . . . . . . 20
7977, 78oveq12d 6099 . . . . . . . . . . . . . . . . . . 19
8079fveq2d 5732 . . . . . . . . . . . . . . . . . 18
8180breq1d 4222 . . . . . . . . . . . . . . . . 17
8281cbvralv 2932 . . . . . . . . . . . . . . . 16
83 fveq2 5728 . . . . . . . . . . . . . . . . . . . . 21
8483fveq1d 5730 . . . . . . . . . . . . . . . . . . . 20
8584oveq1d 6096 . . . . . . . . . . . . . . . . . . 19
8685fveq2d 5732 . . . . . . . . . . . . . . . . . 18
8786breq1d 4222 . . . . . . . . . . . . . . . . 17
8887ralbidv 2725 . . . . . . . . . . . . . . . 16
8982, 88syl5bb 249 . . . . . . . . . . . . . . 15
9076, 89raleqbidv 2916 . . . . . . . . . . . . . 14
9175, 90syl5bb 249 . . . . . . . . . . . . 13
9291cbvralv 2932 . . . . . . . . . . . 12
93 fveq2 5728 . . . . . . . . . . . . 13
9493raleqdv 2910 . . . . . . . . . . . 12
9592, 94syl5bb 249 . . . . . . . . . . 11
9695cbvrexv 2933 . . . . . . . . . 10
9774, 96syl6bbr 255 . . . . . . . . 9
9897rspccva 3051 . . . . . . . 8
9969, 70, 98syl2an 464 . . . . . . 7
1003uztrn2 10503 . . . . . . . . . . 11
101 eqid 2436 . . . . . . . . . . . . . 14
102 eluzelz 10496 . . . . . . . . . . . . . . . 16
103102, 3eleq2s 2528 . . . . . . . . . . . . . . 15
104103ad2antlr 708 . . . . . . . . . . . . . 14
10570adantl 453 . . . . . . . . . . . . . . 15
106105ad2antrr 707 . . . . . . . . . . . . . 14
107 simplr 732 . . . . . . . . . . . . . . . 16
1083uztrn2 10503 . . . . . . . . . . . . . . . 16
109107, 108sylan 458 . . . . . . . . . . . . . . 15
110 fveq2 5728 . . . . . . . . . . . . . . . . 17
111110fveq1d 5730 . . . . . . . . . . . . . . . 16
112 eqid 2436 . . . . . . . . . . . . . . . 16
113 fvex 5742 . . . . . . . . . . . . . . . 16
114111, 112, 113fvmpt 5806 . . . . . . . . . . . . . . 15
115109, 114syl 16 . . . . . . . . . . . . . 14
1166adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
117116ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . . . 24
118 elmapi 7038 . . . . . . . . . . . . . . . . . . . . . . . 24
119117, 118syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
120119ffvelrnda 5870 . . . . . . . . . . . . . . . . . . . . . 22
121120an32s 780 . . . . . . . . . . . . . . . . . . . . 21
122 eqid 2436 . . . . . . . . . . . . . . . . . . . . 21
123121, 122fmptd 5893 . . . . . . . . . . . . . . . . . . . 20
124123ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19
125 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
127125, 126oveq12d 6099 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128127fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
129128breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26
130129rspcv 3048 . . . . . . . . . . . . . . . . . . . . . . . . 25
131130ralimdv 2785 . . . . . . . . . . . . . . . . . . . . . . . 24
132131reximdv 2817 . . . . . . . . . . . . . . . . . . . . . . 23
133132ralimdv 2785 . . . . . . . . . . . . . . . . . . . . . 22
134133impcom 420 . . . . . . . . . . . . . . . . . . . . 21
135134adantll 695 . . . . . . . . . . . . . . . . . . . 20
136 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137136oveq1d 6096 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138137fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
139138breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26
140139cbvralv 2932 . . . . . . . . . . . . . . . . . . . . . . . . 25
141 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142141oveq2d 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143142fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
144143breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . . 26
14593, 144raleqbidv 2916 . . . . . . . . . . . . . . . . . . . . . . . . 25
146140, 145syl5bb 249 . . . . . . . . . . . . . . . . . . . . . . . 24
147146cbvrexv 2933 . . . . . . . . . . . . . . . . . . . . . . 23
148 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
149148fveq1d 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150 fvex 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
151149, 122, 150fvmpt 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
15239, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
153 fveq2 5728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
154153fveq1d 5730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155 fvex 5742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
156154, 122, 155fvmpt 5806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157156adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
158152, 157oveq12d 6099 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
159158fveq2d 5732 . . . . . . . . . . . . . . . . . . . . . . . . . 26
160159breq1d 4222 . . . . . . . . . . . . . . . . . . . . . . . . 25
161160ralbidva 2721 . . . . . . . . . . . . . . . . . . . . . . . 24
162161rexbiia 2738 . . . . . . . . . . . . . . . . . . . . . . 23
163147, 162bitri 241 . . . . . . . . . . . . . . . . . . . . . 22
164 breq2 4216 . . . . . . . . . . . . . . . . . . . . . . . 24
165164ralbidv 2725 . . . . . . . . . . . . . . . . . . . . . . 23
166165rexbidv 2726 . . . . . . . . . . . . . . . . . . . . . 22
167163, 166syl5bb 249 . . . . . . . . . . . . . . . . . . . . 21
168167cbvralv 2932 . . . . . . . . . . . . . . . . . . . 20
169135, 168sylibr 204 . . . . . . . . . . . . . . . . . . 19
170 fvex 5742 . . . . . . . . . . . . . . . . . . . . . 22
1713, 170eqeltri 2506 . . . . . . . . . . . . . . . . . . . . 21
172171mptex 5966 . . . . . . . . . . . . . . . . . . . 20
173172a1i 11 . . . . . . . . . . . . . . . . . . 19
1743, 124, 169, 173caucvg 12472 . . . . . . . . . . . . . . . . . 18
175174ralrimiva 2789 . . . . . . . . . . . . . . . . 17
176175ad2antrr 707 . . . . . . . . . . . . . . . 16
177 fveq2 5728 . . . . . . . . . . . . . . . . . . 19
178177mpteq2dv 4296 . . . . . . . . . . . . . . . . . 18
179178eleq1d 2502 . . . . . . . . . . . . . . . . 17
180179rspccva 3051 . . . . . . . . . . . . . . . 16
181176, 180sylan 458 . . . . . . . . . . . . . . 15
182 climdm 12348 . . . . . . . . . . . . . . 15
183181, 182sylib 189 . . . . . . . . . . . . . 14
184101, 104, 106, 115, 183climi2 12305 . . . . . . . . . . . . 13
185101r19.29uz 12154 . . . . . . . . . . . . . . 15
186101r19.2uz 12155 . . . . . . . . . . . . . . 15
187185, 186syl 16 . . . . . . . . . . . . . 14
1886ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20
189188ffvelrnda 5870 . . . . . . . . . . . . . . . . . . 19
190 elmapi 7038 . . . . . . . . . . . . . . . . . . 19
191189, 190syl 16 . . . . . . . . . . . . . . . . . 18
192191ffvelrnda 5870 . . . . . . . . . . . . . . . . 17
193192adantr 452 . . . . . . . . . . . . . . . 16
194 climcl 12293 . . . . . . . . . . . . . . . . . 18
195183, 194syl 16 . . . . . . . . . . . . . . . . 17
196195adantr 452 . . . . . . . . . . . . . . . 16
1976ad5antr 715 . . . . . . . . . . . . . . . . . . 19
198197, 109ffvelrnd 5871 . . . . . . . . . . . . . . . . . 18
199 elmapi 7038 . . . . . . . . . . . . . . . . . 18
200198, 199syl 16 . . . . . . . . . . . . . . . . 17
201 simplr 732 . . . . . . . . . . . . . . . . 17
202200, 201ffvelrnd 5871 . . . . . . . . . . . . . . . 16
203 rpre 10618 . . . . . . . . . . . . . . . . 17
204203ad4antlr 714 . . . . . . . . . . . . . . . 16
205 abs3lem 12142 . . . . . . . . . . . . . . . 16
206193, 196, 202, 204, 205syl22anc 1185 . . . . . . . . . . . . . . 15
207206rexlimdva 2830 . . . . . . . . . . . . . 14
208187, 207syl5 30 . . . . . . . . . . . . 13
209184, 208mpan2d 656 . . . . . . . . . . . 12
210209ralimdva 2784 . . . . . . . . . . 11
211100, 210sylan2 461 . . . . . . . . . 10
212211anassrs 630 . . . . . . . . 9
213212ralimdva 2784 . . . . . . . 8
214213reximdva 2818 . . . . . . 7
21599, 214mpd 15 . . . . . 6
216215ralrimiva 2789 . . . . 5
2174adantr 452 . . . . . 6
218 eqidd 2437 . . . . . 6
219178fveq2d 5732 . . . . . . . 8
220 eqid 2436 . . . . . . . 8
221 fvex 5742 . . . . . . . 8
222219, 220, 221fvmpt 5806 . . . . . . 7
223222adantl 453 . . . . . 6
224 climdm 12348 . . . . . . . . 9
225174, 224sylib 189 . . . . . . . 8
226 climcl 12293 . . . . . . . 8