ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 23399

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 23400 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 5049	. . . 4
2	1	ibi 249	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 737	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 737	. . . . . . . 8 $/\$ $/\$
8		eqidd 2463	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2463	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 767	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 11356	. . . . . . . . 9
12	11	adantl 472	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 23390	. . . . . . 7 $/\$ $/\$
14		simpr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2550	. . . . . . . . . 10 $/\$ $/\$ $/\$
16		eluzelz 11197	. . . . . . . . . 10
17		uzid 11202	. . . . . . . . . 10
18		fveq2 5888	. . . . . . . . . . . . . . . 16
19	18	fveq1d 5890	. . . . . . . . . . . . . . 15
20	19	oveq1d 6330	. . . . . . . . . . . . . 14
21	20	fveq2d 5892	. . . . . . . . . . . . 13
22	21	breq1d 4426	. . . . . . . . . . . 12
23	22	ralbidv 2839	. . . . . . . . . . 11
24	23	rspcv 3158	. . . . . . . . . 10
25	15, 16, 17, 24	4syl 19	. . . . . . . . 9 $/\$ $/\$ $/\$
26		r19.26 2929	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	7	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
28	27	adantr 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
29		elmapi 7519	. . . . . . . . . . . . . . . . . . . . . . 23
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
31	30	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
32		ulmcl 23385	. . . . . . . . . . . . . . . . . . . . . . 23
33	32	ad4antlr 744	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
34	33	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
35	31, 34	abssubd 13564	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq1d 4426	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	biimpd 212	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
38	3	uztrn2 11205	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39		ffvelrn 6043	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	7, 38, 39	syl2an 484	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
41	40	anassrs 658	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
42		elmapi 7519	. . . . . . . . . . . . . . . . . . . . 21
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
44	43	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
45		rpre 11337	. . . . . . . . . . . . . . . . . . . 20
46	45	ad4antlr 744	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
47		abs3lem 13450	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
48	44, 31, 34, 46, 47	syl22anc 1277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	37, 48	sylan2d 489	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	ancomsd 460	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ralimdva 2808	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
52	26, 51	syl5bir 226	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	expdimp 443	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	an32s 818	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ralimdva 2808	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
56	55	ex 440	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	com23 81	. . . . . . . . 9 $/\$ $/\$ $/\$
58	25, 57	mpdd 41	. . . . . . . 8 $/\$ $/\$ $/\$
59	58	reximdva 2874	. . . . . . 7 $/\$ $/\$
60	13, 59	mpd 15	. . . . . 6 $/\$ $/\$
61	60	ralrimiva 2814	. . . . 5 $/\$
62	61	ex 440	. . . 4
63	62	exlimdv 1790	. . 3
64	2, 63	syl5 33	. 2
65		ulmrel 23382	. . . 4
66		ulmcau.s	. . . . . . . . . 10
67	3, 4, 66, 6	ulmcaulem 23398	. . . . . . . . 9
68	67	biimpa 491	. . . . . . . 8 $/\$
69		rphalfcl 11356	. . . . . . . 8
70		breq2 4420	. . . . . . . . . . . . 13
71	70	ralbidv 2839	. . . . . . . . . . . 12
72	71	2ralbidv 2844	. . . . . . . . . . 11
73	72	rexbidv 2913	. . . . . . . . . 10
74		ralcom 2963	. . . . . . . . . . . . . 14
75		fveq2 5888	. . . . . . . . . . . . . . 15
76		fveq2 5888	. . . . . . . . . . . . . . . . . . . 20
77		fveq2 5888	. . . . . . . . . . . . . . . . . . . 20
78	76, 77	oveq12d 6333	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5892	. . . . . . . . . . . . . . . . . 18
80	79	breq1d 4426	. . . . . . . . . . . . . . . . 17
81	80	cbvralv 3031	. . . . . . . . . . . . . . . 16
82		fveq2 5888	. . . . . . . . . . . . . . . . . . . . 21
83	82	fveq1d 5890	. . . . . . . . . . . . . . . . . . . 20
84	83	oveq1d 6330	. . . . . . . . . . . . . . . . . . 19
85	84	fveq2d 5892	. . . . . . . . . . . . . . . . . 18
86	85	breq1d 4426	. . . . . . . . . . . . . . . . 17
87	86	ralbidv 2839	. . . . . . . . . . . . . . . 16
88	81, 87	syl5bb 265	. . . . . . . . . . . . . . 15
89	75, 88	raleqbidv 3013	. . . . . . . . . . . . . 14
90	74, 89	syl5bb 265	. . . . . . . . . . . . 13
91	90	cbvralv 3031	. . . . . . . . . . . 12
92		fveq2 5888	. . . . . . . . . . . . 13
93	92	raleqdv 3005	. . . . . . . . . . . 12
94	91, 93	syl5bb 265	. . . . . . . . . . 11
95	94	cbvrexv 3032	. . . . . . . . . 10
96	73, 95	syl6bbr 271	. . . . . . . . 9
97	96	rspccva 3161	. . . . . . . 8 $/\$
98	68, 69, 97	syl2an 484	. . . . . . 7 $/\$ $/\$
99	3	uztrn2 11205	. . . . . . . . . . 11 $/\$
100		eqid 2462	. . . . . . . . . . . . . 14
101		eluzelz 11197	. . . . . . . . . . . . . . . 16
102	101, 3	eleq2s 2558	. . . . . . . . . . . . . . 15
103	102	ad2antlr 738	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	69	adantl 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	ad2antrr 737	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106		simplr 767	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
107	3	uztrn2 11205	. . . . . . . . . . . . . . . 16 $/\$
108	106, 107	sylan 478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
109		fveq2 5888	. . . . . . . . . . . . . . . . 17
110	109	fveq1d 5890	. . . . . . . . . . . . . . . 16
111		eqid 2462	. . . . . . . . . . . . . . . 16
112		fvex 5898	. . . . . . . . . . . . . . . 16
113	110, 111, 112	fvmpt 5971	. . . . . . . . . . . . . . 15
114	108, 113	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	6	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	115	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
117		elmapi 7519	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	119	an32s 818	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
121		eqid 2462	. . . . . . . . . . . . . . . . . . . . 21
122	120, 121	fmptd 6069	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123	122	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126	124, 125	oveq12d 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127	126	fveq2d 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
128	127	breq1d 4426	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	rspcv 3158	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	129	ralimdv 2810	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	reximdv 2873	. . . . . . . . . . . . . . . . . . . . . . 23
132	131	ralimdv 2810	. . . . . . . . . . . . . . . . . . . . . 22
133	132	impcom 436	. . . . . . . . . . . . . . . . . . . . 21 $/\$
134	133	adantll 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	135	oveq1d 6330	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	fveq2d 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	137	breq1d 4426	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	cbvralv 3031	. . . . . . . . . . . . . . . . . . . . . . . . 25
140		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141	140	oveq2d 6331	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142	141	fveq2d 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143	142	breq1d 4426	. . . . . . . . . . . . . . . . . . . . . . . . . 26
144	92, 143	raleqbidv 3013	. . . . . . . . . . . . . . . . . . . . . . . . 25
145	139, 144	syl5bb 265	. . . . . . . . . . . . . . . . . . . . . . . 24
146	145	cbvrexv 3032	. . . . . . . . . . . . . . . . . . . . . . 23
147		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148	147	fveq1d 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149		fvex 5898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150	148, 121, 149	fvmpt 5971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	38, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152		fveq2 5888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
153	152	fveq1d 5890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
154		fvex 5898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	153, 121, 154	fvmpt 5971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
156	155	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
157	151, 156	oveq12d 6333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
158	157	fveq2d 5892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
159	158	breq1d 4426	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	159	ralbidva 2836	. . . . . . . . . . . . . . . . . . . . . . . 24
161	160	rexbiia 2900	. . . . . . . . . . . . . . . . . . . . . . 23
162	146, 161	bitri 257	. . . . . . . . . . . . . . . . . . . . . 22
163		breq2 4420	. . . . . . . . . . . . . . . . . . . . . . . 24
164	163	ralbidv 2839	. . . . . . . . . . . . . . . . . . . . . . 23
165	164	rexbidv 2913	. . . . . . . . . . . . . . . . . . . . . 22
166	162, 165	syl5bb 265	. . . . . . . . . . . . . . . . . . . . 21
167	166	cbvralv 3031	. . . . . . . . . . . . . . . . . . . 20
168	134, 167	sylibr 217	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		fvex 5898	. . . . . . . . . . . . . . . . . . . . . 22
170	3, 169	eqeltri 2536	. . . . . . . . . . . . . . . . . . . . 21
171	170	mptex 6161	. . . . . . . . . . . . . . . . . . . 20
172	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	3, 123, 168, 172	caucvg 13794	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
174	173	ralrimiva 2814	. . . . . . . . . . . . . . . . 17 $/\$
175	174	ad2antrr 737	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		fveq2 5888	. . . . . . . . . . . . . . . . . . 19
177	176	mpteq2dv 4504	. . . . . . . . . . . . . . . . . 18
178	177	eleq1d 2524	. . . . . . . . . . . . . . . . 17
179	178	rspccva 3161	. . . . . . . . . . . . . . . 16 $/\$
180	175, 179	sylan 478	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181		climdm 13667	. . . . . . . . . . . . . . 15
182	180, 181	sylib 201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	100, 103, 105, 114, 182	climi2 13624	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
184	100	r19.29uz 13462	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	100	r19.2uz 13463	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	184, 185	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
187	6	ad2antrr 737	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
188	187	ffvelrnda 6045	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
189		elmapi 7519	. . . . . . . . . . . . . . . . . . 19
190	188, 189	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	190	ffvelrnda 6045	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
193		climcl 13612	. . . . . . . . . . . . . . . . . 18
194	182, 193	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
195	194	adantr 471	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
196	6	ad5antr 745	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
197	196, 108	ffvelrnd 6046	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
198		elmapi 7519	. . . . . . . . . . . . . . . . . 18
199	197, 198	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
200		simplr 767	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201	199, 200	ffvelrnd 6046	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
202		rpre 11337	. . . . . . . . . . . . . . . . 17
203	202	ad4antlr 744	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
204		abs3lem 13450	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
205	192, 195, 201, 203, 204	syl22anc 1277	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdva 2891	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
207	186, 206	syl5 33	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
208	183, 207	mpan2d 685	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
209	208	ralimdva 2808	. . . . . . . . . . 11 $/\$ $/\$ $/\$
210	99, 209	sylan2 481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
211	210	anassrs 658	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
212	211	ralimdva 2808	. . . . . . . 8 $/\$ $/\$ $/\$
213	212	reximdva 2874	. . . . . . 7 $/\$ $/\$
214	98, 213	mpd 15	. . . . . 6 $/\$ $/\$
215	214	ralrimiva 2814	. . . . 5 $/\$
216	4	adantr 471	. . . . . 6 $/\$
217		eqidd 2463	. . . . . 6 $/\$ $/\$ $/\$
218	177	fveq2d 5892	. . . . . . . 8
219		eqid 2462	. . . . . . . 8
220		fvex 5898	. . . . . . . 8
221	218, 219, 220	fvmpt 5971	. . . . . . 7
222	221	adantl 472	. . . . . 6 $/\$ $/\$
223		climdm 13667	. . . . . . . . 9
224	173, 223	sylib 201	. . . . . . . 8 $/\$ $/\$
225		climcl 13612	. . . . . . . 8
226	224, 225	syl 17	. . . . . . 7 $/\$