ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 21860

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 21861 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 5035	. . . 4
2	1	ibi 241	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 725	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 725	. . . . . . . 8 $/\$ $/\$
8		eqidd 2444	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2444	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 754	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 11015	. . . . . . . . 9
12	11	adantl 466	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 21851	. . . . . . 7 $/\$ $/\$
14		simpr 461	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2533	. . . . . . . . . 10 $/\$ $/\$ $/\$
16		eluzelz 10870	. . . . . . . . . 10
17		uzid 10875	. . . . . . . . . 10
18		fveq2 5691	. . . . . . . . . . . . . . . 16
19	18	fveq1d 5693	. . . . . . . . . . . . . . 15
20	19	oveq1d 6106	. . . . . . . . . . . . . 14
21	20	fveq2d 5695	. . . . . . . . . . . . 13
22	21	breq1d 4302	. . . . . . . . . . . 12
23	22	ralbidv 2735	. . . . . . . . . . 11
24	23	rspcv 3069	. . . . . . . . . 10
25	15, 16, 17, 24	4syl 21	. . . . . . . . 9 $/\$ $/\$ $/\$
26		r19.26 2849	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	7	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
28	27	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
29		elmapi 7234	. . . . . . . . . . . . . . . . . . . . . . 23
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
31	30	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
32		ulmcl 21846	. . . . . . . . . . . . . . . . . . . . . . 23
33	32	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
34	33	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
35	31, 34	abssubd 12939	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq1d 4302	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	biimpd 207	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
38	3	uztrn2 10878	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39		ffvelrn 5841	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	7, 38, 39	syl2an 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
41	40	anassrs 648	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
42		elmapi 7234	. . . . . . . . . . . . . . . . . . . . 21
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
44	43	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
45		rpre 10997	. . . . . . . . . . . . . . . . . . . 20
46	45	ad4antlr 732	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
47		abs3lem 12826	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
48	44, 31, 34, 46, 47	syl22anc 1219	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	37, 48	sylan2d 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	ancomsd 454	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ralimdva 2794	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
52	26, 51	syl5bir 218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	expdimp 437	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	an32s 802	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ralimdva 2794	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
56	55	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	com23 78	. . . . . . . . 9 $/\$ $/\$ $/\$
58	25, 57	mpdd 40	. . . . . . . 8 $/\$ $/\$ $/\$
59	58	reximdva 2828	. . . . . . 7 $/\$ $/\$
60	13, 59	mpd 15	. . . . . 6 $/\$ $/\$
61	60	ralrimiva 2799	. . . . 5 $/\$
62	61	ex 434	. . . 4
63	62	exlimdv 1690	. . 3
64	2, 63	syl5 32	. 2
65		ulmrel 21843	. . . 4
66		ulmcau.s	. . . . . . . . . 10
67	3, 4, 66, 6	ulmcaulem 21859	. . . . . . . . 9
68	67	biimpa 484	. . . . . . . 8 $/\$
69		rphalfcl 11015	. . . . . . . 8
70		breq2 4296	. . . . . . . . . . . . 13
71	70	ralbidv 2735	. . . . . . . . . . . 12
72	71	2ralbidv 2757	. . . . . . . . . . 11
73	72	rexbidv 2736	. . . . . . . . . 10
74		ralcom 2881	. . . . . . . . . . . . . 14
75		fveq2 5691	. . . . . . . . . . . . . . 15
76		fveq2 5691	. . . . . . . . . . . . . . . . . . . 20
77		fveq2 5691	. . . . . . . . . . . . . . . . . . . 20
78	76, 77	oveq12d 6109	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5695	. . . . . . . . . . . . . . . . . 18
80	79	breq1d 4302	. . . . . . . . . . . . . . . . 17
81	80	cbvralv 2947	. . . . . . . . . . . . . . . 16
82		fveq2 5691	. . . . . . . . . . . . . . . . . . . . 21
83	82	fveq1d 5693	. . . . . . . . . . . . . . . . . . . 20
84	83	oveq1d 6106	. . . . . . . . . . . . . . . . . . 19
85	84	fveq2d 5695	. . . . . . . . . . . . . . . . . 18
86	85	breq1d 4302	. . . . . . . . . . . . . . . . 17
87	86	ralbidv 2735	. . . . . . . . . . . . . . . 16
88	81, 87	syl5bb 257	. . . . . . . . . . . . . . 15
89	75, 88	raleqbidv 2931	. . . . . . . . . . . . . 14
90	74, 89	syl5bb 257	. . . . . . . . . . . . 13
91	90	cbvralv 2947	. . . . . . . . . . . 12
92		fveq2 5691	. . . . . . . . . . . . 13
93	92	raleqdv 2923	. . . . . . . . . . . 12
94	91, 93	syl5bb 257	. . . . . . . . . . 11
95	94	cbvrexv 2948	. . . . . . . . . 10
96	73, 95	syl6bbr 263	. . . . . . . . 9
97	96	rspccva 3072	. . . . . . . 8 $/\$
98	68, 69, 97	syl2an 477	. . . . . . 7 $/\$ $/\$
99	3	uztrn2 10878	. . . . . . . . . . 11 $/\$
100		eqid 2443	. . . . . . . . . . . . . 14
101		eluzelz 10870	. . . . . . . . . . . . . . . 16
102	101, 3	eleq2s 2535	. . . . . . . . . . . . . . 15
103	102	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	69	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	ad2antrr 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
107	3	uztrn2 10878	. . . . . . . . . . . . . . . 16 $/\$
108	106, 107	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
109		fveq2 5691	. . . . . . . . . . . . . . . . 17
110	109	fveq1d 5693	. . . . . . . . . . . . . . . 16
111		eqid 2443	. . . . . . . . . . . . . . . 16
112		fvex 5701	. . . . . . . . . . . . . . . 16
113	110, 111, 112	fvmpt 5774	. . . . . . . . . . . . . . 15
114	108, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	6	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	115	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
117		elmapi 7234	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	119	an32s 802	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
121		eqid 2443	. . . . . . . . . . . . . . . . . . . . 21
122	120, 121	fmptd 5867	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123	122	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126	124, 125	oveq12d 6109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127	126	fveq2d 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
128	127	breq1d 4302	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	rspcv 3069	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	129	ralimdv 2795	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	reximdv 2827	. . . . . . . . . . . . . . . . . . . . . . 23
132	131	ralimdv 2795	. . . . . . . . . . . . . . . . . . . . . 22
133	132	impcom 430	. . . . . . . . . . . . . . . . . . . . 21 $/\$
134	133	adantll 713	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	135	oveq1d 6106	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	fveq2d 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	137	breq1d 4302	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	cbvralv 2947	. . . . . . . . . . . . . . . . . . . . . . . . 25
140		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141	140	oveq2d 6107	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142	141	fveq2d 5695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143	142	breq1d 4302	. . . . . . . . . . . . . . . . . . . . . . . . . 26
144	92, 143	raleqbidv 2931	. . . . . . . . . . . . . . . . . . . . . . . . 25
145	139, 144	syl5bb 257	. . . . . . . . . . . . . . . . . . . . . . . 24
146	145	cbvrexv 2948	. . . . . . . . . . . . . . . . . . . . . . 23
147		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148	147	fveq1d 5693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150	148, 121, 149	fvmpt 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	38, 150	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
153	152	fveq1d 5693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
154		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	153, 121, 154	fvmpt 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
156	155	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
157	151, 156	oveq12d 6109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
158	157	fveq2d 5695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
159	158	breq1d 4302	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	159	ralbidva 2731	. . . . . . . . . . . . . . . . . . . . . . . 24
161	160	rexbiia 2748	. . . . . . . . . . . . . . . . . . . . . . 23
162	146, 161	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22
163		breq2 4296	. . . . . . . . . . . . . . . . . . . . . . . 24
164	163	ralbidv 2735	. . . . . . . . . . . . . . . . . . . . . . 23
165	164	rexbidv 2736	. . . . . . . . . . . . . . . . . . . . . 22
166	162, 165	syl5bb 257	. . . . . . . . . . . . . . . . . . . . 21
167	166	cbvralv 2947	. . . . . . . . . . . . . . . . . . . 20
168	134, 167	sylibr 212	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		fvex 5701	. . . . . . . . . . . . . . . . . . . . . 22
170	3, 169	eqeltri 2513	. . . . . . . . . . . . . . . . . . . . 21
171	170	mptex 5948	. . . . . . . . . . . . . . . . . . . 20
172	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	3, 123, 168, 172	caucvg 13156	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
174	173	ralrimiva 2799	. . . . . . . . . . . . . . . . 17 $/\$
175	174	ad2antrr 725	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		fveq2 5691	. . . . . . . . . . . . . . . . . . 19
177	176	mpteq2dv 4379	. . . . . . . . . . . . . . . . . 18
178	177	eleq1d 2509	. . . . . . . . . . . . . . . . 17
179	178	rspccva 3072	. . . . . . . . . . . . . . . 16 $/\$
180	175, 179	sylan 471	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181		climdm 13032	. . . . . . . . . . . . . . 15
182	180, 181	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	100, 103, 105, 114, 182	climi2 12989	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
184	100	r19.29uz 12838	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	100	r19.2uz 12839	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	184, 185	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
187	6	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
188	187	ffvelrnda 5843	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
189		elmapi 7234	. . . . . . . . . . . . . . . . . . 19
190	188, 189	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	190	ffvelrnda 5843	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
193		climcl 12977	. . . . . . . . . . . . . . . . . 18
194	182, 193	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
195	194	adantr 465	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
196	6	ad5antr 733	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
197	196, 108	ffvelrnd 5844	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
198		elmapi 7234	. . . . . . . . . . . . . . . . . 18
199	197, 198	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
200		simplr 754	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201	199, 200	ffvelrnd 5844	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
202		rpre 10997	. . . . . . . . . . . . . . . . 17
203	202	ad4antlr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
204		abs3lem 12826	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
205	192, 195, 201, 203, 204	syl22anc 1219	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdva 2841	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
207	186, 206	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
208	183, 207	mpan2d 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
209	208	ralimdva 2794	. . . . . . . . . . 11 $/\$ $/\$ $/\$
210	99, 209	sylan2 474	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
211	210	anassrs 648	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
212	211	ralimdva 2794	. . . . . . . 8 $/\$ $/\$ $/\$
213	212	reximdva 2828	. . . . . . 7 $/\$ $/\$
214	98, 213	mpd 15	. . . . . 6 $/\$ $/\$
215	214	ralrimiva 2799	. . . . 5 $/\$
216	4	adantr 465	. . . . . 6 $/\$
217		eqidd 2444	. . . . . 6 $/\$ $/\$ $/\$
218	177	fveq2d 5695	. . . . . . . 8
219		eqid 2443	. . . . . . . 8
220		fvex 5701	. . . . . . . 8
221	218, 219, 220	fvmpt 5774	. . . . . . 7
222	221	adantl 466	. . . . . 6 $/\$ $/\$
223		climdm 13032	. . . . . . . . 9
224	173, 223	sylib 196	. . . . . . . 8 $/\$ $/\$
225		climcl 12977	. . . . . . . 8
226	224, 225	syl 16	. . . . . . 7 $/\$