ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 20264

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 20265 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.

Step	Hyp	Ref	Expression
1		eldmg 5024	. . . 4
2	1	ibi 233	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 707	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 707	. . . . . . . 8 $/\$ $/\$
8		eqidd 2405	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2405	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 732	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 10592	. . . . . . . . 9
12	11	adantl 453	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 20255	. . . . . . 7 $/\$ $/\$
14		simpr 448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2494	. . . . . . . . . . 11 $/\$ $/\$ $/\$
16		eluzelz 10452	. . . . . . . . . . 11
17		uzid 10456	. . . . . . . . . . 11
18	15, 16, 17	3syl 19	. . . . . . . . . 10 $/\$ $/\$ $/\$
19		fveq2 5687	. . . . . . . . . . . . . . . 16
20	19	fveq1d 5689	. . . . . . . . . . . . . . 15
21	20	oveq1d 6055	. . . . . . . . . . . . . 14
22	21	fveq2d 5691	. . . . . . . . . . . . 13
23	22	breq1d 4182	. . . . . . . . . . . 12
24	23	ralbidv 2686	. . . . . . . . . . 11
25	24	rspcv 3008	. . . . . . . . . 10
26	18, 25	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
27		r19.26 2798	. . . . . . . . . . . . . . 15 $/\$ $/\$
28	7	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
29	28	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
30		elmapi 6997	. . . . . . . . . . . . . . . . . . . . . . 23
31	29, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
32	31	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
33		ulmcl 20250	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	ad4antlr 714	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
35	34	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
36	32, 35	abssubd 12210	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	breq1d 4182	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
38	37	biimpd 199	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
39	3	uztrn2 10459	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40		ffvelrn 5827	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
41	7, 39, 40	syl2an 464	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
42	41	anassrs 630	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
43		elmapi 6997	. . . . . . . . . . . . . . . . . . . . 21
44	42, 43	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
45	44	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
46		rpre 10574	. . . . . . . . . . . . . . . . . . . 20
47	46	ad4antlr 714	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
48		abs3lem 12097	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
49	45, 32, 35, 47, 48	syl22anc 1185	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	38, 49	sylan2d 469	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ancomsd 441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	51	ralimdva 2744	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
53	27, 52	syl5bir 210	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	expdimp 427	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	an32s 780	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
56	55	ralimdva 2744	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
57	56	ex 424	. . . . . . . . . 10 $/\$ $/\$ $/\$
58	57	com23 74	. . . . . . . . 9 $/\$ $/\$ $/\$
59	26, 58	mpdd 38	. . . . . . . 8 $/\$ $/\$ $/\$
60	59	reximdva 2778	. . . . . . 7 $/\$ $/\$
61	13, 60	mpd 15	. . . . . 6 $/\$ $/\$
62	61	ralrimiva 2749	. . . . 5 $/\$
63	62	ex 424	. . . 4
64	63	exlimdv 1643	. . 3
65	2, 64	syl5 30	. 2
66		ulmrel 20247	. . . 4
67		ulmcau.s	. . . . . . . . . 10
68	3, 4, 67, 6	ulmcaulem 20263	. . . . . . . . 9
69	68	biimpa 471	. . . . . . . 8 $/\$
70		rphalfcl 10592	. . . . . . . 8
71		breq2 4176	. . . . . . . . . . . . 13
72	71	ralbidv 2686	. . . . . . . . . . . 12
73	72	2ralbidv 2708	. . . . . . . . . . 11
74	73	rexbidv 2687	. . . . . . . . . 10
75		ralcom 2828	. . . . . . . . . . . . . 14
76		fveq2 5687	. . . . . . . . . . . . . . 15
77		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20
78		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20
79	77, 78	oveq12d 6058	. . . . . . . . . . . . . . . . . . 19
80	79	fveq2d 5691	. . . . . . . . . . . . . . . . . 18
81	80	breq1d 4182	. . . . . . . . . . . . . . . . 17
82	81	cbvralv 2892	. . . . . . . . . . . . . . . 16
83		fveq2 5687	. . . . . . . . . . . . . . . . . . . . 21
84	83	fveq1d 5689	. . . . . . . . . . . . . . . . . . . 20
85	84	oveq1d 6055	. . . . . . . . . . . . . . . . . . 19
86	85	fveq2d 5691	. . . . . . . . . . . . . . . . . 18
87	86	breq1d 4182	. . . . . . . . . . . . . . . . 17
88	87	ralbidv 2686	. . . . . . . . . . . . . . . 16
89	82, 88	syl5bb 249	. . . . . . . . . . . . . . 15
90	76, 89	raleqbidv 2876	. . . . . . . . . . . . . 14
91	75, 90	syl5bb 249	. . . . . . . . . . . . 13
92	91	cbvralv 2892	. . . . . . . . . . . 12
93		fveq2 5687	. . . . . . . . . . . . 13
94	93	raleqdv 2870	. . . . . . . . . . . 12
95	92, 94	syl5bb 249	. . . . . . . . . . 11
96	95	cbvrexv 2893	. . . . . . . . . 10
97	74, 96	syl6bbr 255	. . . . . . . . 9
98	97	rspccva 3011	. . . . . . . 8 $/\$
99	69, 70, 98	syl2an 464	. . . . . . 7 $/\$ $/\$
100	3	uztrn2 10459	. . . . . . . . . . 11 $/\$
101		eqid 2404	. . . . . . . . . . . . . 14
102		eluzelz 10452	. . . . . . . . . . . . . . . 16
103	102, 3	eleq2s 2496	. . . . . . . . . . . . . . 15
104	103	ad2antlr 708	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
105	70	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$
106	105	ad2antrr 707	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
107		simplr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
108	3	uztrn2 10459	. . . . . . . . . . . . . . . 16 $/\$
109	107, 108	sylan 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
110		fveq2 5687	. . . . . . . . . . . . . . . . 17
111	110	fveq1d 5689	. . . . . . . . . . . . . . . 16
112		eqid 2404	. . . . . . . . . . . . . . . 16
113		fvex 5701	. . . . . . . . . . . . . . . 16
114	111, 112, 113	fvmpt 5765	. . . . . . . . . . . . . . 15
115	109, 114	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
116	6	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
117	116	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
118		elmapi 6997	. . . . . . . . . . . . . . . . . . . . . . . 24
119	117, 118	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
120	119	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
121	120	an32s 780	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
122		eqid 2404	. . . . . . . . . . . . . . . . . . . . 21
123	121, 122	fmptd 5852	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
124	123	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
127	125, 126	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
128	127	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	128	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130	129	rspcv 3008	. . . . . . . . . . . . . . . . . . . . . . . . 25
131	130	ralimdv 2745	. . . . . . . . . . . . . . . . . . . . . . . 24
132	131	reximdv 2777	. . . . . . . . . . . . . . . . . . . . . . 23
133	132	ralimdv 2745	. . . . . . . . . . . . . . . . . . . . . 22
134	133	impcom 420	. . . . . . . . . . . . . . . . . . . . 21 $/\$
135	134	adantll 695	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
136		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137	136	oveq1d 6055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138	137	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
139	138	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . . 26
140	139	cbvralv 2892	. . . . . . . . . . . . . . . . . . . . . . . . 25
141		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
142	141	oveq2d 6056	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143	142	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
144	143	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . . 26
145	93, 144	raleqbidv 2876	. . . . . . . . . . . . . . . . . . . . . . . . 25
146	140, 145	syl5bb 249	. . . . . . . . . . . . . . . . . . . . . . . 24
147	146	cbvrexv 2893	. . . . . . . . . . . . . . . . . . . . . . 23
148		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
149	148	fveq1d 5689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
151	149, 122, 150	fvmpt 5765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
152	39, 151	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
153		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
154	153	fveq1d 5689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
156	154, 122, 155	fvmpt 5765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157	156	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
158	152, 157	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
159	158	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
160	159	breq1d 4182	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
161	160	ralbidva 2682	. . . . . . . . . . . . . . . . . . . . . . . 24
162	161	rexbiia 2699	. . . . . . . . . . . . . . . . . . . . . . 23
163	147, 162	bitri 241	. . . . . . . . . . . . . . . . . . . . . 22
164		breq2 4176	. . . . . . . . . . . . . . . . . . . . . . . 24
165	164	ralbidv 2686	. . . . . . . . . . . . . . . . . . . . . . 23
166	165	rexbidv 2687	. . . . . . . . . . . . . . . . . . . . . 22
167	163, 166	syl5bb 249	. . . . . . . . . . . . . . . . . . . . 21
168	167	cbvralv 2892	. . . . . . . . . . . . . . . . . . . 20
169	135, 168	sylibr 204	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
170		fvex 5701	. . . . . . . . . . . . . . . . . . . . . 22
171	3, 170	eqeltri 2474	. . . . . . . . . . . . . . . . . . . . 21
172	171	mptex 5925	. . . . . . . . . . . . . . . . . . . 20
173	172	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
174	3, 124, 169, 173	caucvg 12427	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
175	174	ralrimiva 2749	. . . . . . . . . . . . . . . . 17 $/\$
176	175	ad2antrr 707	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
177		fveq2 5687	. . . . . . . . . . . . . . . . . . 19
178	177	mpteq2dv 4256	. . . . . . . . . . . . . . . . . 18
179	178	eleq1d 2470	. . . . . . . . . . . . . . . . 17
180	179	rspccva 3011	. . . . . . . . . . . . . . . 16 $/\$
181	176, 180	sylan 458	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
182		climdm 12303	. . . . . . . . . . . . . . 15
183	181, 182	sylib 189	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
184	101, 104, 106, 115, 183	climi2 12260	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
185	101	r19.29uz 12109	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	101	r19.2uz 12110	. . . . . . . . . . . . . . 15 $/\$ $/\$
187	185, 186	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
188	6	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
189	188	ffvelrnda 5829	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
190		elmapi 6997	. . . . . . . . . . . . . . . . . . 19
191	189, 190	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
192	191	ffvelrnda 5829	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
193	192	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
194		climcl 12248	. . . . . . . . . . . . . . . . . 18
195	183, 194	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
196	195	adantr 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
197	6	ad5antr 715	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
198	197, 109	ffvelrnd 5830	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
199		elmapi 6997	. . . . . . . . . . . . . . . . . 18
200	198, 199	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201		simplr 732	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
202	200, 201	ffvelrnd 5830	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
203		rpre 10574	. . . . . . . . . . . . . . . . 17
204	203	ad4antlr 714	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
205		abs3lem 12097	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
206	193, 196, 202, 204, 205	syl22anc 1185	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
207	206	rexlimdva 2790	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
208	187, 207	syl5 30	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
209	184, 208	mpan2d 656	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
210	209	ralimdva 2744	. . . . . . . . . . 11 $/\$ $/\$ $/\$
211	100, 210	sylan2 461	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
212	211	anassrs 630	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
213	212	ralimdva 2744	. . . . . . . 8 $/\$ $/\$ $/\$
214	213	reximdva 2778	. . . . . . 7 $/\$ $/\$
215	99, 214	mpd 15	. . . . . 6 $/\$ $/\$
216	215	ralrimiva 2749	. . . . 5 $/\$
217	4	adantr 452	. . . . . 6 $/\$
218		eqidd 2405	. . . . . 6 $/\$ $/\$ $/\$
219	178	fveq2d 5691	. . . . . . . 8
220		eqid 2404	. . . . . . . 8
221		fvex 5701	. . . . . . . 8
222	219, 220, 221	fvmpt 5765	. . . . . . 7
223	222	adantl 453	. . . . . 6 $/\$ $/\$
224		climdm 12303	. . . . . . . . 9
225	174, 224	sylib 189	. . . . . . . 8 $/\$ $/\$
226		climcl 12248	. . . . . . . 8