ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 23215

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 23216 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 5050	. . . 4
2	1	ibi 244	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 730	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 730	. . . . . . . 8 $/\$ $/\$
8		eqidd 2430	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2430	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 760	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 11327	. . . . . . . . 9
12	11	adantl 467	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 23206	. . . . . . 7 $/\$ $/\$
14		simpr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2527	. . . . . . . . . 10 $/\$ $/\$ $/\$
16		eluzelz 11168	. . . . . . . . . 10
17		uzid 11173	. . . . . . . . . 10
18		fveq2 5881	. . . . . . . . . . . . . . . 16
19	18	fveq1d 5883	. . . . . . . . . . . . . . 15
20	19	oveq1d 6320	. . . . . . . . . . . . . 14
21	20	fveq2d 5885	. . . . . . . . . . . . 13
22	21	breq1d 4436	. . . . . . . . . . . 12
23	22	ralbidv 2871	. . . . . . . . . . 11
24	23	rspcv 3184	. . . . . . . . . 10
25	15, 16, 17, 24	4syl 19	. . . . . . . . 9 $/\$ $/\$ $/\$
26		r19.26 2962	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	7	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
28	27	adantr 466	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
29		elmapi 7501	. . . . . . . . . . . . . . . . . . . . . . 23
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
31	30	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
32		ulmcl 23201	. . . . . . . . . . . . . . . . . . . . . . 23
33	32	ad4antlr 737	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
34	33	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
35	31, 34	abssubd 13493	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq1d 4436	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	biimpd 210	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
38	3	uztrn2 11176	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39		ffvelrn 6035	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	7, 38, 39	syl2an 479	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
41	40	anassrs 652	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
42		elmapi 7501	. . . . . . . . . . . . . . . . . . . . 21
43	41, 42	syl 17	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
44	43	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
45		rpre 11308	. . . . . . . . . . . . . . . . . . . 20
46	45	ad4antlr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
47		abs3lem 13380	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
48	44, 31, 34, 46, 47	syl22anc 1265	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	37, 48	sylan2d 484	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	ancomsd 455	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ralimdva 2840	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
52	26, 51	syl5bir 221	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	expdimp 438	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	an32s 811	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ralimdva 2840	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
56	55	ex 435	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	com23 81	. . . . . . . . 9 $/\$ $/\$ $/\$
58	25, 57	mpdd 41	. . . . . . . 8 $/\$ $/\$ $/\$
59	58	reximdva 2907	. . . . . . 7 $/\$ $/\$
60	13, 59	mpd 15	. . . . . 6 $/\$ $/\$
61	60	ralrimiva 2846	. . . . 5 $/\$
62	61	ex 435	. . . 4
63	62	exlimdv 1771	. . 3
64	2, 63	syl5 33	. 2
65		ulmrel 23198	. . . 4
66		ulmcau.s	. . . . . . . . . 10
67	3, 4, 66, 6	ulmcaulem 23214	. . . . . . . . 9
68	67	biimpa 486	. . . . . . . 8 $/\$
69		rphalfcl 11327	. . . . . . . 8
70		breq2 4430	. . . . . . . . . . . . 13
71	70	ralbidv 2871	. . . . . . . . . . . 12
72	71	2ralbidv 2876	. . . . . . . . . . 11
73	72	rexbidv 2946	. . . . . . . . . 10
74		ralcom 2996	. . . . . . . . . . . . . 14
75		fveq2 5881	. . . . . . . . . . . . . . 15
76		fveq2 5881	. . . . . . . . . . . . . . . . . . . 20
77		fveq2 5881	. . . . . . . . . . . . . . . . . . . 20
78	76, 77	oveq12d 6323	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5885	. . . . . . . . . . . . . . . . . 18
80	79	breq1d 4436	. . . . . . . . . . . . . . . . 17
81	80	cbvralv 3062	. . . . . . . . . . . . . . . 16
82		fveq2 5881	. . . . . . . . . . . . . . . . . . . . 21
83	82	fveq1d 5883	. . . . . . . . . . . . . . . . . . . 20
84	83	oveq1d 6320	. . . . . . . . . . . . . . . . . . 19
85	84	fveq2d 5885	. . . . . . . . . . . . . . . . . 18
86	85	breq1d 4436	. . . . . . . . . . . . . . . . 17
87	86	ralbidv 2871	. . . . . . . . . . . . . . . 16
88	81, 87	syl5bb 260	. . . . . . . . . . . . . . 15
89	75, 88	raleqbidv 3046	. . . . . . . . . . . . . 14
90	74, 89	syl5bb 260	. . . . . . . . . . . . 13
91	90	cbvralv 3062	. . . . . . . . . . . 12
92		fveq2 5881	. . . . . . . . . . . . 13
93	92	raleqdv 3038	. . . . . . . . . . . 12
94	91, 93	syl5bb 260	. . . . . . . . . . 11
95	94	cbvrexv 3063	. . . . . . . . . 10
96	73, 95	syl6bbr 266	. . . . . . . . 9
97	96	rspccva 3187	. . . . . . . 8 $/\$
98	68, 69, 97	syl2an 479	. . . . . . 7 $/\$ $/\$
99	3	uztrn2 11176	. . . . . . . . . . 11 $/\$
100		eqid 2429	. . . . . . . . . . . . . 14
101		eluzelz 11168	. . . . . . . . . . . . . . . 16
102	101, 3	eleq2s 2537	. . . . . . . . . . . . . . 15
103	102	ad2antlr 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	69	adantl 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	ad2antrr 730	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106		simplr 760	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
107	3	uztrn2 11176	. . . . . . . . . . . . . . . 16 $/\$
108	106, 107	sylan 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
109		fveq2 5881	. . . . . . . . . . . . . . . . 17
110	109	fveq1d 5883	. . . . . . . . . . . . . . . 16
111		eqid 2429	. . . . . . . . . . . . . . . 16
112		fvex 5891	. . . . . . . . . . . . . . . 16
113	110, 111, 112	fvmpt 5964	. . . . . . . . . . . . . . 15
114	108, 113	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	6	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	115	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
117		elmapi 7501	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	119	an32s 811	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
121		eqid 2429	. . . . . . . . . . . . . . . . . . . . 21
122	120, 121	fmptd 6061	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123	122	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126	124, 125	oveq12d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127	126	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
128	127	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	rspcv 3184	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	129	ralimdv 2842	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	reximdv 2906	. . . . . . . . . . . . . . . . . . . . . . 23
132	131	ralimdv 2842	. . . . . . . . . . . . . . . . . . . . . 22
133	132	impcom 431	. . . . . . . . . . . . . . . . . . . . 21 $/\$
134	133	adantll 718	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	135	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	137	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	cbvralv 3062	. . . . . . . . . . . . . . . . . . . . . . . . 25
140		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141	140	oveq2d 6321	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142	141	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143	142	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . . . . 26
144	92, 143	raleqbidv 3046	. . . . . . . . . . . . . . . . . . . . . . . . 25
145	139, 144	syl5bb 260	. . . . . . . . . . . . . . . . . . . . . . . 24
146	145	cbvrexv 3063	. . . . . . . . . . . . . . . . . . . . . . 23
147		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148	147	fveq1d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149		fvex 5891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150	148, 121, 149	fvmpt 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	38, 150	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
153	152	fveq1d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
154		fvex 5891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	153, 121, 154	fvmpt 5964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
156	155	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
157	151, 156	oveq12d 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
158	157	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
159	158	breq1d 4436	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	159	ralbidva 2868	. . . . . . . . . . . . . . . . . . . . . . . 24
161	160	rexbiia 2933	. . . . . . . . . . . . . . . . . . . . . . 23
162	146, 161	bitri 252	. . . . . . . . . . . . . . . . . . . . . 22
163		breq2 4430	. . . . . . . . . . . . . . . . . . . . . . . 24
164	163	ralbidv 2871	. . . . . . . . . . . . . . . . . . . . . . 23
165	164	rexbidv 2946	. . . . . . . . . . . . . . . . . . . . . 22
166	162, 165	syl5bb 260	. . . . . . . . . . . . . . . . . . . . 21
167	166	cbvralv 3062	. . . . . . . . . . . . . . . . . . . 20
168	134, 167	sylibr 215	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		fvex 5891	. . . . . . . . . . . . . . . . . . . . . 22
170	3, 169	eqeltri 2513	. . . . . . . . . . . . . . . . . . . . 21
171	170	mptex 6151	. . . . . . . . . . . . . . . . . . . 20
172	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	3, 123, 168, 172	caucvg 13723	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
174	173	ralrimiva 2846	. . . . . . . . . . . . . . . . 17 $/\$
175	174	ad2antrr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		fveq2 5881	. . . . . . . . . . . . . . . . . . 19
177	176	mpteq2dv 4513	. . . . . . . . . . . . . . . . . 18
178	177	eleq1d 2498	. . . . . . . . . . . . . . . . 17
179	178	rspccva 3187	. . . . . . . . . . . . . . . 16 $/\$
180	175, 179	sylan 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181		climdm 13596	. . . . . . . . . . . . . . 15
182	180, 181	sylib 199	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	100, 103, 105, 114, 182	climi2 13553	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
184	100	r19.29uz 13392	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	100	r19.2uz 13393	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	184, 185	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$
187	6	ad2antrr 730	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
188	187	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
189		elmapi 7501	. . . . . . . . . . . . . . . . . . 19
190	188, 189	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	190	ffvelrnda 6037	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
193		climcl 13541	. . . . . . . . . . . . . . . . . 18
194	182, 193	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
195	194	adantr 466	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
196	6	ad5antr 738	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
197	196, 108	ffvelrnd 6038	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
198		elmapi 7501	. . . . . . . . . . . . . . . . . 18
199	197, 198	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
200		simplr 760	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201	199, 200	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
202		rpre 11308	. . . . . . . . . . . . . . . . 17
203	202	ad4antlr 737	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
204		abs3lem 13380	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
205	192, 195, 201, 203, 204	syl22anc 1265	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdva 2924	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
207	186, 206	syl5 33	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
208	183, 207	mpan2d 678	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
209	208	ralimdva 2840	. . . . . . . . . . 11 $/\$ $/\$ $/\$
210	99, 209	sylan2 476	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
211	210	anassrs 652	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
212	211	ralimdva 2840	. . . . . . . 8 $/\$ $/\$ $/\$
213	212	reximdva 2907	. . . . . . 7 $/\$ $/\$
214	98, 213	mpd 15	. . . . . 6 $/\$ $/\$
215	214	ralrimiva 2846	. . . . 5 $/\$
216	4	adantr 466	. . . . . 6 $/\$
217		eqidd 2430	. . . . . 6 $/\$ $/\$ $/\$
218	177	fveq2d 5885	. . . . . . . 8
219		eqid 2429	. . . . . . . 8
220		fvex 5891	. . . . . . . 8
221	218, 219, 220	fvmpt 5964	. . . . . . 7
222	221	adantl 467	. . . . . 6 $/\$ $/\$
223		climdm 13596	. . . . . . . . 9
224	173, 223	sylib 199	. . . . . . . 8 $/\$ $/\$
225		climcl 13541	. . . . . . . 8
226	224, 225	syl 17	. . . . . . 7 $/\$