ulmcau - Metamath Proof Explorer

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

Theorem ulmcau 22956

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 22957 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 5187	. . . 4
2	1	ibi 241	. . 3
3		ulmcau.z	. . . . . . . 8
4		ulmcau.m	. . . . . . . . 9
5	4	ad2antrr 723	. . . . . . . 8 $/\$ $/\$
6		ulmcau.f	. . . . . . . . 9
7	6	ad2antrr 723	. . . . . . . 8 $/\$ $/\$
8		eqidd 2455	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
9		eqidd 2455	. . . . . . . 8 $/\$ $/\$ $/\$
10		simplr 753	. . . . . . . 8 $/\$ $/\$
11		rphalfcl 11246	. . . . . . . . 9
12	11	adantl 464	. . . . . . . 8 $/\$ $/\$
13	3, 5, 7, 8, 9, 10, 12	ulmi 22947	. . . . . . 7 $/\$ $/\$
14		simpr 459	. . . . . . . . . . 11 $/\$ $/\$ $/\$
15	14, 3	syl6eleq 2552	. . . . . . . . . 10 $/\$ $/\$ $/\$
16		eluzelz 11091	. . . . . . . . . 10
17		uzid 11096	. . . . . . . . . 10
18		fveq2 5848	. . . . . . . . . . . . . . . 16
19	18	fveq1d 5850	. . . . . . . . . . . . . . 15
20	19	oveq1d 6285	. . . . . . . . . . . . . 14
21	20	fveq2d 5852	. . . . . . . . . . . . 13
22	21	breq1d 4449	. . . . . . . . . . . 12
23	22	ralbidv 2893	. . . . . . . . . . 11
24	23	rspcv 3203	. . . . . . . . . 10
25	15, 16, 17, 24	4syl 21	. . . . . . . . 9 $/\$ $/\$ $/\$
26		r19.26 2981	. . . . . . . . . . . . . . 15 $/\$ $/\$
27	7	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
28	27	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
29		elmapi 7433	. . . . . . . . . . . . . . . . . . . . . . 23
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
31	30	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
32		ulmcl 22942	. . . . . . . . . . . . . . . . . . . . . . 23
33	32	ad4antlr 730	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
34	33	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$
35	31, 34	abssubd 13366	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	breq1d 4449	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
37	36	biimpd 207	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
38	3	uztrn2 11099	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39		ffvelrn 6005	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
40	7, 38, 39	syl2an 475	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
41	40	anassrs 646	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
42		elmapi 7433	. . . . . . . . . . . . . . . . . . . . 21
43	41, 42	syl 16	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
44	43	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
45		rpre 11227	. . . . . . . . . . . . . . . . . . . 20
46	45	ad4antlr 730	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
47		abs3lem 13253	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
48	44, 31, 34, 46, 47	syl22anc 1227	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49	37, 48	sylan2d 480	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	49	ancomsd 452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	50	ralimdva 2862	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
52	26, 51	syl5bir 218	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	expdimp 435	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	an32s 802	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
55	54	ralimdva 2862	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
56	55	ex 432	. . . . . . . . . 10 $/\$ $/\$ $/\$
57	56	com23 78	. . . . . . . . 9 $/\$ $/\$ $/\$
58	25, 57	mpdd 40	. . . . . . . 8 $/\$ $/\$ $/\$
59	58	reximdva 2929	. . . . . . 7 $/\$ $/\$
60	13, 59	mpd 15	. . . . . 6 $/\$ $/\$
61	60	ralrimiva 2868	. . . . 5 $/\$
62	61	ex 432	. . . 4
63	62	exlimdv 1729	. . 3
64	2, 63	syl5 32	. 2
65		ulmrel 22939	. . . 4
66		ulmcau.s	. . . . . . . . . 10
67	3, 4, 66, 6	ulmcaulem 22955	. . . . . . . . 9
68	67	biimpa 482	. . . . . . . 8 $/\$
69		rphalfcl 11246	. . . . . . . 8
70		breq2 4443	. . . . . . . . . . . . 13
71	70	ralbidv 2893	. . . . . . . . . . . 12
72	71	2ralbidv 2898	. . . . . . . . . . 11
73	72	rexbidv 2965	. . . . . . . . . 10
74		ralcom 3015	. . . . . . . . . . . . . 14
75		fveq2 5848	. . . . . . . . . . . . . . 15
76		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20
77		fveq2 5848	. . . . . . . . . . . . . . . . . . . 20
78	76, 77	oveq12d 6288	. . . . . . . . . . . . . . . . . . 19
79	78	fveq2d 5852	. . . . . . . . . . . . . . . . . 18
80	79	breq1d 4449	. . . . . . . . . . . . . . . . 17
81	80	cbvralv 3081	. . . . . . . . . . . . . . . 16
82		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21
83	82	fveq1d 5850	. . . . . . . . . . . . . . . . . . . 20
84	83	oveq1d 6285	. . . . . . . . . . . . . . . . . . 19
85	84	fveq2d 5852	. . . . . . . . . . . . . . . . . 18
86	85	breq1d 4449	. . . . . . . . . . . . . . . . 17
87	86	ralbidv 2893	. . . . . . . . . . . . . . . 16
88	81, 87	syl5bb 257	. . . . . . . . . . . . . . 15
89	75, 88	raleqbidv 3065	. . . . . . . . . . . . . 14
90	74, 89	syl5bb 257	. . . . . . . . . . . . 13
91	90	cbvralv 3081	. . . . . . . . . . . 12
92		fveq2 5848	. . . . . . . . . . . . 13
93	92	raleqdv 3057	. . . . . . . . . . . 12
94	91, 93	syl5bb 257	. . . . . . . . . . 11
95	94	cbvrexv 3082	. . . . . . . . . 10
96	73, 95	syl6bbr 263	. . . . . . . . 9
97	96	rspccva 3206	. . . . . . . 8 $/\$
98	68, 69, 97	syl2an 475	. . . . . . 7 $/\$ $/\$
99	3	uztrn2 11099	. . . . . . . . . . 11 $/\$
100		eqid 2454	. . . . . . . . . . . . . 14
101		eluzelz 11091	. . . . . . . . . . . . . . . 16
102	101, 3	eleq2s 2562	. . . . . . . . . . . . . . 15
103	102	ad2antlr 724	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
104	69	adantl 464	. . . . . . . . . . . . . . 15 $/\$ $/\$
105	104	ad2antrr 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
106		simplr 753	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
107	3	uztrn2 11099	. . . . . . . . . . . . . . . 16 $/\$
108	106, 107	sylan 469	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
109		fveq2 5848	. . . . . . . . . . . . . . . . 17
110	109	fveq1d 5850	. . . . . . . . . . . . . . . 16
111		eqid 2454	. . . . . . . . . . . . . . . 16
112		fvex 5858	. . . . . . . . . . . . . . . 16
113	110, 111, 112	fvmpt 5931	. . . . . . . . . . . . . . 15
114	108, 113	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
115	6	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
116	115	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
117		elmapi 7433	. . . . . . . . . . . . . . . . . . . . . . . 24
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
119	118	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
120	119	an32s 802	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
121		eqid 2454	. . . . . . . . . . . . . . . . . . . . 21
122	120, 121	fmptd 6031	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123	122	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
124		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
126	124, 125	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
127	126	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
128	127	breq1d 4449	. . . . . . . . . . . . . . . . . . . . . . . . . 26
129	128	rspcv 3203	. . . . . . . . . . . . . . . . . . . . . . . . 25
130	129	ralimdv 2864	. . . . . . . . . . . . . . . . . . . . . . . 24
131	130	reximdv 2928	. . . . . . . . . . . . . . . . . . . . . . 23
132	131	ralimdv 2864	. . . . . . . . . . . . . . . . . . . . . 22
133	132	impcom 428	. . . . . . . . . . . . . . . . . . . . 21 $/\$
134	133	adantll 711	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
135		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136	135	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
137	136	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
138	137	breq1d 4449	. . . . . . . . . . . . . . . . . . . . . . . . . 26
139	138	cbvralv 3081	. . . . . . . . . . . . . . . . . . . . . . . . 25
140		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
141	140	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
142	141	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
143	142	breq1d 4449	. . . . . . . . . . . . . . . . . . . . . . . . . 26
144	92, 143	raleqbidv 3065	. . . . . . . . . . . . . . . . . . . . . . . . 25
145	139, 144	syl5bb 257	. . . . . . . . . . . . . . . . . . . . . . . 24
146	145	cbvrexv 3082	. . . . . . . . . . . . . . . . . . . . . . 23
147		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
148	147	fveq1d 5850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
149		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
150	148, 121, 149	fvmpt 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	38, 150	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
152		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
153	152	fveq1d 5850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
154		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
155	153, 121, 154	fvmpt 5931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
156	155	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
157	151, 156	oveq12d 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
158	157	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
159	158	breq1d 4449	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
160	159	ralbidva 2890	. . . . . . . . . . . . . . . . . . . . . . . 24
161	160	rexbiia 2955	. . . . . . . . . . . . . . . . . . . . . . 23
162	146, 161	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22
163		breq2 4443	. . . . . . . . . . . . . . . . . . . . . . . 24
164	163	ralbidv 2893	. . . . . . . . . . . . . . . . . . . . . . 23
165	164	rexbidv 2965	. . . . . . . . . . . . . . . . . . . . . 22
166	162, 165	syl5bb 257	. . . . . . . . . . . . . . . . . . . . 21
167	166	cbvralv 3081	. . . . . . . . . . . . . . . . . . . 20
168	134, 167	sylibr 212	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
169		fvex 5858	. . . . . . . . . . . . . . . . . . . . . 22
170	3, 169	eqeltri 2538	. . . . . . . . . . . . . . . . . . . . 21
171	170	mptex 6118	. . . . . . . . . . . . . . . . . . . 20
172	171	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
173	3, 123, 168, 172	caucvg 13583	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
174	173	ralrimiva 2868	. . . . . . . . . . . . . . . . 17 $/\$
175	174	ad2antrr 723	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
176		fveq2 5848	. . . . . . . . . . . . . . . . . . 19
177	176	mpteq2dv 4526	. . . . . . . . . . . . . . . . . 18
178	177	eleq1d 2523	. . . . . . . . . . . . . . . . 17
179	178	rspccva 3206	. . . . . . . . . . . . . . . 16 $/\$
180	175, 179	sylan 469	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
181		climdm 13459	. . . . . . . . . . . . . . 15
182	180, 181	sylib 196	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
183	100, 103, 105, 114, 182	climi2 13416	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
184	100	r19.29uz 13265	. . . . . . . . . . . . . . 15 $/\$ $/\$
185	100	r19.2uz 13266	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	184, 185	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$
187	6	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
188	187	ffvelrnda 6007	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
189		elmapi 7433	. . . . . . . . . . . . . . . . . . 19
190	188, 189	syl 16	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
191	190	ffvelrnda 6007	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
192	191	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
193		climcl 13404	. . . . . . . . . . . . . . . . . 18
194	182, 193	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
195	194	adantr 463	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
196	6	ad5antr 731	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
197	196, 108	ffvelrnd 6008	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
198		elmapi 7433	. . . . . . . . . . . . . . . . . 18
199	197, 198	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
200		simplr 753	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
201	199, 200	ffvelrnd 6008	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
202		rpre 11227	. . . . . . . . . . . . . . . . 17
203	202	ad4antlr 730	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
204		abs3lem 13253	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
205	192, 195, 201, 203, 204	syl22anc 1227	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
206	205	rexlimdva 2946	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
207	186, 206	syl5 32	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
208	183, 207	mpan2d 672	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
209	208	ralimdva 2862	. . . . . . . . . . 11 $/\$ $/\$ $/\$
210	99, 209	sylan2 472	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
211	210	anassrs 646	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
212	211	ralimdva 2862	. . . . . . . 8 $/\$ $/\$ $/\$
213	212	reximdva 2929	. . . . . . 7 $/\$ $/\$
214	98, 213	mpd 15	. . . . . 6 $/\$ $/\$
215	214	ralrimiva 2868	. . . . 5 $/\$
216	4	adantr 463	. . . . . 6 $/\$
217		eqidd 2455	. . . . . 6 $/\$ $/\$ $/\$
218	177	fveq2d 5852	. . . . . . . 8
219		eqid 2454	. . . . . . . 8
220		fvex 5858	. . . . . . . 8
221	218, 219, 220	fvmpt 5931	. . . . . . 7
222	221	adantl 464	. . . . . 6 $/\$ $/\$
223		climdm 13459	. . . . . . . . 9
224	173, 223	sylib 196	. . . . . . . 8 $/\$ $/\$
225		climcl 13404	. . . . . . . 8
226	224, 225	syl 16	. . . . . . 7 $/\$