ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 21803

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 21804 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 5031	. . . 4
2	1	ibi 241	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 720	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 720	. . . . . . . 8 $/\$ $/\$
8		eqidd 2442	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2442	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 749	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 11011	. . . . . . . . 9
12	11	adantl 463	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 21794	. . . . . . 7 $/\$ $/\$
14		simpr 458	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2531	. . . . . . . . . 10 $/\$ $/\$ $/\$
16		eluzelz 10866	. . . . . . . . . 10
17		uzid 10871	. . . . . . . . . 10
18		fveq2 5688	. . . . . . . . . . . . . . . 16
19	18	fveq1d 5690	. . . . . . . . . . . . . . 15
20	19	oveq1d 6105	. . . . . . . . . . . . . 14
21	20	fveq2d 5692	. . . . . . . . . . . . 13
22	21	breq1d 4299	. . . . . . . . . . . 12
23	22	ralbidv 2733	. . . . . . . . . . 11
24	23	rspcv 3066	. . . . . . . . . 10
25	15, 16, 17, 24	4syl 21	. . . . . . . . 9 $/\$ $/\$ $/\$
26		r19.26 2847	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	7	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
28	27	adantr 462	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
29		elmapi 7230	. . . . . . . . . . . . . . . . . . . . . . 23
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
31	30	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
32		ulmcl 21789	. . . . . . . . . . . . . . . . . . . . . . 23
33	32	ad4antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
34	33	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
35	31, 34	abssubd 12935	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq1d 4299	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	biimpd 207	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
38	3	uztrn2 10874	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39		ffvelrn 5838	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	7, 38, 39	syl2an 474	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
41	40	anassrs 643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
42		elmapi 7230	. . . . . . . . . . . . . . . . . . . . 21
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
44	43	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
45		rpre 10993	. . . . . . . . . . . . . . . . . . . 20
46	45	ad4antlr 727	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
47		abs3lem 12822	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
48	44, 31, 34, 46, 47	syl22anc 1214	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	37, 48	sylan2d 479	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	ancomsd 451	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ralimdva 2792	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
52	26, 51	syl5bir 218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	expdimp 437	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	an32s 797	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ralimdva 2792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
56	55	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	com23 78	. . . . . . . . 9 $/\$ $/\$ $/\$
58	25, 57	mpdd 40	. . . . . . . 8 $/\$ $/\$ $/\$
59	58	reximdva 2826	. . . . . . 7 $/\$ $/\$
60	13, 59	mpd 15	. . . . . 6 $/\$ $/\$
61	60	ralrimiva 2797	. . . . 5 $/\$
62	61	ex 434	. . . 4
63	62	exlimdv 1695	. . 3
64	2, 63	syl5 32	. 2
65		ulmrel 21786	. . . 4
66		ulmcau.s	. . . . . . . . . 10
67	3, 4, 66, 6	ulmcaulem 21802	. . . . . . . . 9
68	67	biimpa 481	. . . . . . . 8 $/\$
69		rphalfcl 11011	. . . . . . . 8
70		breq2 4293	. . . . . . . . . . . . 13
71	70	ralbidv 2733	. . . . . . . . . . . 12
72	71	2ralbidv 2755	. . . . . . . . . . 11
73	72	rexbidv 2734	. . . . . . . . . 10
74		ralcom 2879	. . . . . . . . . . . . . 14
75		fveq2 5688	. . . . . . . . . . . . . . 15
76		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20
77		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20
78	76, 77	oveq12d 6108	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5692	. . . . . . . . . . . . . . . . . 18
80	79	breq1d 4299	. . . . . . . . . . . . . . . . 17
81	80	cbvralv 2945	. . . . . . . . . . . . . . . 16
82		fveq2 5688	. . . . . . . . . . . . . . . . . . . . 21
83	82	fveq1d 5690	. . . . . . . . . . . . . . . . . . . 20
84	83	oveq1d 6105	. . . . . . . . . . . . . . . . . . 19
85	84	fveq2d 5692	. . . . . . . . . . . . . . . . . 18
86	85	breq1d 4299	. . . . . . . . . . . . . . . . 17
87	86	ralbidv 2733	. . . . . . . . . . . . . . . 16
88	81, 87	syl5bb 257	. . . . . . . . . . . . . . 15
89	75, 88	raleqbidv 2929	. . . . . . . . . . . . . 14
90	74, 89	syl5bb 257	. . . . . . . . . . . . 13
91	90	cbvralv 2945	. . . . . . . . . . . 12
92		fveq2 5688	. . . . . . . . . . . . 13
93	92	raleqdv 2921	. . . . . . . . . . . 12
94	91, 93	syl5bb 257	. . . . . . . . . . 11
95	94	cbvrexv 2946	. . . . . . . . . 10
96	73, 95	syl6bbr 263	. . . . . . . . 9
97	96	rspccva 3069	. . . . . . . 8 $/\$
98	68, 69, 97	syl2an 474	. . . . . . 7 $/\$ $/\$
99	3	uztrn2 10874	. . . . . . . . . . 11 $/\$
100		eqid 2441	. . . . . . . . . . . . . 14
101		eluzelz 10866	. . . . . . . . . . . . . . . 16
102	101, 3	eleq2s 2533	. . . . . . . . . . . . . . 15
103	102	ad2antlr 721	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	69	adantl 463	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	ad2antrr 720	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106		simplr 749	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
107	3	uztrn2 10874	. . . . . . . . . . . . . . . 16 $/\$
108	106, 107	sylan 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
109		fveq2 5688	. . . . . . . . . . . . . . . . 17
110	109	fveq1d 5690	. . . . . . . . . . . . . . . 16
111		eqid 2441	. . . . . . . . . . . . . . . 16
112		fvex 5698	. . . . . . . . . . . . . . . 16
113	110, 111, 112	fvmpt 5771	. . . . . . . . . . . . . . 15
114	108, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	6	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	115	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
117		elmapi 7230	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	119	an32s 797	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
121		eqid 2441	. . . . . . . . . . . . . . . . . . . . 21
122	120, 121	fmptd 5864	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123	122	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126	124, 125	oveq12d 6108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127	126	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
128	127	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	rspcv 3066	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	129	ralimdv 2793	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	reximdv 2825	. . . . . . . . . . . . . . . . . . . . . . 23
132	131	ralimdv 2793	. . . . . . . . . . . . . . . . . . . . . 22
133	132	impcom 430	. . . . . . . . . . . . . . . . . . . . 21 $/\$
134	133	adantll 708	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	135	oveq1d 6105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	137	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	cbvralv 2945	. . . . . . . . . . . . . . . . . . . . . . . . 25
140		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141	140	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142	141	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143	142	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . 26
144	92, 143	raleqbidv 2929	. . . . . . . . . . . . . . . . . . . . . . . . 25
145	139, 144	syl5bb 257	. . . . . . . . . . . . . . . . . . . . . . . 24
146	145	cbvrexv 2946	. . . . . . . . . . . . . . . . . . . . . . 23
147		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148	147	fveq1d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149		fvex 5698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150	148, 121, 149	fvmpt 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	38, 150	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
153	152	fveq1d 5690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
154		fvex 5698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	153, 121, 154	fvmpt 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
156	155	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
157	151, 156	oveq12d 6108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
158	157	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
159	158	breq1d 4299	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	159	ralbidva 2729	. . . . . . . . . . . . . . . . . . . . . . . 24
161	160	rexbiia 2746	. . . . . . . . . . . . . . . . . . . . . . 23
162	146, 161	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22
163		breq2 4293	. . . . . . . . . . . . . . . . . . . . . . . 24
164	163	ralbidv 2733	. . . . . . . . . . . . . . . . . . . . . . 23
165	164	rexbidv 2734	. . . . . . . . . . . . . . . . . . . . . 22
166	162, 165	syl5bb 257	. . . . . . . . . . . . . . . . . . . . 21
167	166	cbvralv 2945	. . . . . . . . . . . . . . . . . . . 20
168	134, 167	sylibr 212	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		fvex 5698	. . . . . . . . . . . . . . . . . . . . . 22
170	3, 169	eqeltri 2511	. . . . . . . . . . . . . . . . . . . . 21
171	170	mptex 5945	. . . . . . . . . . . . . . . . . . . 20
172	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	3, 123, 168, 172	caucvg 13152	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
174	173	ralrimiva 2797	. . . . . . . . . . . . . . . . 17 $/\$
175	174	ad2antrr 720	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		fveq2 5688	. . . . . . . . . . . . . . . . . . 19
177	176	mpteq2dv 4376	. . . . . . . . . . . . . . . . . 18
178	177	eleq1d 2507	. . . . . . . . . . . . . . . . 17
179	178	rspccva 3069	. . . . . . . . . . . . . . . 16 $/\$
180	175, 179	sylan 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181		climdm 13028	. . . . . . . . . . . . . . 15
182	180, 181	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	100, 103, 105, 114, 182	climi2 12985	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
184	100	r19.29uz 12834	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	100	r19.2uz 12835	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	184, 185	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
187	6	ad2antrr 720	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
188	187	ffvelrnda 5840	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
189		elmapi 7230	. . . . . . . . . . . . . . . . . . 19
190	188, 189	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	190	ffvelrnda 5840	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
193		climcl 12973	. . . . . . . . . . . . . . . . . 18
194	182, 193	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
195	194	adantr 462	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
196	6	ad5antr 728	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
197	196, 108	ffvelrnd 5841	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
198		elmapi 7230	. . . . . . . . . . . . . . . . . 18
199	197, 198	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
200		simplr 749	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201	199, 200	ffvelrnd 5841	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
202		rpre 10993	. . . . . . . . . . . . . . . . 17
203	202	ad4antlr 727	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
204		abs3lem 12822	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
205	192, 195, 201, 203, 204	syl22anc 1214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdva 2839	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
207	186, 206	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
208	183, 207	mpan2d 669	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
209	208	ralimdva 2792	. . . . . . . . . . 11 $/\$ $/\$ $/\$
210	99, 209	sylan2 471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
211	210	anassrs 643	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
212	211	ralimdva 2792	. . . . . . . 8 $/\$ $/\$ $/\$
213	212	reximdva 2826	. . . . . . 7 $/\$ $/\$
214	98, 213	mpd 15	. . . . . 6 $/\$ $/\$
215	214	ralrimiva 2797	. . . . 5 $/\$
216	4	adantr 462	. . . . . 6 $/\$
217		eqidd 2442	. . . . . 6 $/\$ $/\$ $/\$
218	177	fveq2d 5692	. . . . . . . 8
219		eqid 2441	. . . . . . . 8
220		fvex 5698	. . . . . . . 8
221	218, 219, 220	fvmpt 5771	. . . . . . 7
222	221	adantl 463	. . . . . 6 $/\$ $/\$
223		climdm 13028	. . . . . . . . 9
224	173, 223	sylib 196	. . . . . . . 8 $/\$ $/\$
225		climcl 12973	. . . . . . . 8
226	224, 225	syl 16	. . . . . . 7 $/\$