Metamath Proof Explorer


Theorem ulmcau

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k the functions F ( k ) and F ( j ) are uniformly within x of each other on S . This is the four-quantifier version, see ulmcau2 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses ulmcau.z Z = M
ulmcau.m φ M
ulmcau.s φ S V
ulmcau.f φ F : Z S
Assertion ulmcau φ F dom u S x + j Z k j z S F k z F j z < x

Proof

Step Hyp Ref Expression
1 ulmcau.z Z = M
2 ulmcau.m φ M
3 ulmcau.s φ S V
4 ulmcau.f φ F : Z S
5 eldmg F dom u S F dom u S g F u S g
6 5 ibi F dom u S g F u S g
7 2 ad2antrr φ F u S g x + M
8 4 ad2antrr φ F u S g x + F : Z S
9 eqidd φ F u S g x + k Z z S F k z = F k z
10 eqidd φ F u S g x + z S g z = g z
11 simplr φ F u S g x + F u S g
12 rphalfcl x + x 2 +
13 12 adantl φ F u S g x + x 2 +
14 1 7 8 9 10 11 13 ulmi φ F u S g x + j Z k j z S F k z g z < x 2
15 simpr φ F u S g x + j Z j Z
16 15 1 eleqtrdi φ F u S g x + j Z j M
17 eluzelz j M j
18 uzid j j j
19 fveq2 k = j F k = F j
20 19 fveq1d k = j F k z = F j z
21 20 fvoveq1d k = j F k z g z = F j z g z
22 21 breq1d k = j F k z g z < x 2 F j z g z < x 2
23 22 ralbidv k = j z S F k z g z < x 2 z S F j z g z < x 2
24 23 rspcv j j k j z S F k z g z < x 2 z S F j z g z < x 2
25 16 17 18 24 4syl φ F u S g x + j Z k j z S F k z g z < x 2 z S F j z g z < x 2
26 r19.26 z S F j z g z < x 2 F k z g z < x 2 z S F j z g z < x 2 z S F k z g z < x 2
27 8 ffvelrnda φ F u S g x + j Z F j S
28 27 adantr φ F u S g x + j Z k j F j S
29 elmapi F j S F j : S
30 28 29 syl φ F u S g x + j Z k j F j : S
31 30 ffvelrnda φ F u S g x + j Z k j z S F j z
32 ulmcl F u S g g : S
33 32 ad4antlr φ F u S g x + j Z k j g : S
34 33 ffvelrnda φ F u S g x + j Z k j z S g z
35 31 34 abssubd φ F u S g x + j Z k j z S F j z g z = g z F j z
36 35 breq1d φ F u S g x + j Z k j z S F j z g z < x 2 g z F j z < x 2
37 36 biimpd φ F u S g x + j Z k j z S F j z g z < x 2 g z F j z < x 2
38 1 uztrn2 j Z k j k Z
39 ffvelrn F : Z S k Z F k S
40 8 38 39 syl2an φ F u S g x + j Z k j F k S
41 40 anassrs φ F u S g x + j Z k j F k S
42 elmapi F k S F k : S
43 41 42 syl φ F u S g x + j Z k j F k : S
44 43 ffvelrnda φ F u S g x + j Z k j z S F k z
45 rpre x + x
46 45 ad4antlr φ F u S g x + j Z k j z S x
47 abs3lem F k z F j z g z x F k z g z < x 2 g z F j z < x 2 F k z F j z < x
48 44 31 34 46 47 syl22anc φ F u S g x + j Z k j z S F k z g z < x 2 g z F j z < x 2 F k z F j z < x
49 37 48 sylan2d φ F u S g x + j Z k j z S F k z g z < x 2 F j z g z < x 2 F k z F j z < x
50 49 ancomsd φ F u S g x + j Z k j z S F j z g z < x 2 F k z g z < x 2 F k z F j z < x
51 50 ralimdva φ F u S g x + j Z k j z S F j z g z < x 2 F k z g z < x 2 z S F k z F j z < x
52 26 51 syl5bir φ F u S g x + j Z k j z S F j z g z < x 2 z S F k z g z < x 2 z S F k z F j z < x
53 52 expdimp φ F u S g x + j Z k j z S F j z g z < x 2 z S F k z g z < x 2 z S F k z F j z < x
54 53 an32s φ F u S g x + j Z z S F j z g z < x 2 k j z S F k z g z < x 2 z S F k z F j z < x
55 54 ralimdva φ F u S g x + j Z z S F j z g z < x 2 k j z S F k z g z < x 2 k j z S F k z F j z < x
56 55 ex φ F u S g x + j Z z S F j z g z < x 2 k j z S F k z g z < x 2 k j z S F k z F j z < x
57 56 com23 φ F u S g x + j Z k j z S F k z g z < x 2 z S F j z g z < x 2 k j z S F k z F j z < x
58 25 57 mpdd φ F u S g x + j Z k j z S F k z g z < x 2 k j z S F k z F j z < x
59 58 reximdva φ F u S g x + j Z k j z S F k z g z < x 2 j Z k j z S F k z F j z < x
60 14 59 mpd φ F u S g x + j Z k j z S F k z F j z < x
61 60 ralrimiva φ F u S g x + j Z k j z S F k z F j z < x
62 61 ex φ F u S g x + j Z k j z S F k z F j z < x
63 62 exlimdv φ g F u S g x + j Z k j z S F k z F j z < x
64 6 63 syl5 φ F dom u S x + j Z k j z S F k z F j z < x
65 ulmrel Rel u S
66 1 2 3 4 ulmcaulem φ x + j Z k j z S F k z F j z < x x + j Z k j m k z S F k z F m z < x
67 66 biimpa φ x + j Z k j z S F k z F j z < x x + j Z k j m k z S F k z F m z < x
68 rphalfcl r + r 2 +
69 breq2 x = r 2 F k z F m z < x F k z F m z < r 2
70 69 ralbidv x = r 2 z S F k z F m z < x z S F k z F m z < r 2
71 70 2ralbidv x = r 2 k j m k z S F k z F m z < x k j m k z S F k z F m z < r 2
72 71 rexbidv x = r 2 j Z k j m k z S F k z F m z < x j Z k j m k z S F k z F m z < r 2
73 ralcom w S m q F q w F m w < r 2 m q w S F q w F m w < r 2
74 fveq2 q = k q = k
75 fveq2 w = z F q w = F q z
76 fveq2 w = z F m w = F m z
77 75 76 oveq12d w = z F q w F m w = F q z F m z
78 77 fveq2d w = z F q w F m w = F q z F m z
79 78 breq1d w = z F q w F m w < r 2 F q z F m z < r 2
80 79 cbvralvw w S F q w F m w < r 2 z S F q z F m z < r 2
81 fveq2 q = k F q = F k
82 81 fveq1d q = k F q z = F k z
83 82 fvoveq1d q = k F q z F m z = F k z F m z
84 83 breq1d q = k F q z F m z < r 2 F k z F m z < r 2
85 84 ralbidv q = k z S F q z F m z < r 2 z S F k z F m z < r 2
86 80 85 syl5bb q = k w S F q w F m w < r 2 z S F k z F m z < r 2
87 74 86 raleqbidv q = k m q w S F q w F m w < r 2 m k z S F k z F m z < r 2
88 73 87 syl5bb q = k w S m q F q w F m w < r 2 m k z S F k z F m z < r 2
89 88 cbvralvw q p w S m q F q w F m w < r 2 k p m k z S F k z F m z < r 2
90 fveq2 p = j p = j
91 90 raleqdv p = j k p m k z S F k z F m z < r 2 k j m k z S F k z F m z < r 2
92 89 91 syl5bb p = j q p w S m q F q w F m w < r 2 k j m k z S F k z F m z < r 2
93 92 cbvrexvw p Z q p w S m q F q w F m w < r 2 j Z k j m k z S F k z F m z < r 2
94 72 93 bitr4di x = r 2 j Z k j m k z S F k z F m z < x p Z q p w S m q F q w F m w < r 2
95 94 rspccva x + j Z k j m k z S F k z F m z < x r 2 + p Z q p w S m q F q w F m w < r 2
96 67 68 95 syl2an φ x + j Z k j z S F k z F j z < x r + p Z q p w S m q F q w F m w < r 2
97 1 uztrn2 p Z q p q Z
98 eqid q = q
99 eluzelz q M q
100 99 1 eleq2s q Z q
101 100 ad2antlr φ x + j Z k j z S F k z F j z < x r + q Z w S q
102 68 adantl φ x + j Z k j z S F k z F j z < x r + r 2 +
103 102 ad2antrr φ x + j Z k j z S F k z F j z < x r + q Z w S r 2 +
104 simplr φ x + j Z k j z S F k z F j z < x r + q Z w S q Z
105 1 uztrn2 q Z m q m Z
106 104 105 sylan φ x + j Z k j z S F k z F j z < x r + q Z w S m q m Z
107 fveq2 n = m F n = F m
108 107 fveq1d n = m F n w = F m w
109 eqid n Z F n w = n Z F n w
110 fvex F m w V
111 108 109 110 fvmpt m Z n Z F n w m = F m w
112 106 111 syl φ x + j Z k j z S F k z F j z < x r + q Z w S m q n Z F n w m = F m w
113 4 adantr φ x + j Z k j z S F k z F j z < x F : Z S
114 113 ffvelrnda φ x + j Z k j z S F k z F j z < x n Z F n S
115 elmapi F n S F n : S
116 114 115 syl φ x + j Z k j z S F k z F j z < x n Z F n : S
117 116 ffvelrnda φ x + j Z k j z S F k z F j z < x n Z y S F n y
118 117 an32s φ x + j Z k j z S F k z F j z < x y S n Z F n y
119 118 fmpttd φ x + j Z k j z S F k z F j z < x y S n Z F n y : Z
120 119 ffvelrnda φ x + j Z k j z S F k z F j z < x y S q Z n Z F n y q
121 fveq2 z = y F k z = F k y
122 fveq2 z = y F j z = F j y
123 121 122 oveq12d z = y F k z F j z = F k y F j y
124 123 fveq2d z = y F k z F j z = F k y F j y
125 124 breq1d z = y F k z F j z < x F k y F j y < x
126 125 rspcv y S z S F k z F j z < x F k y F j y < x
127 126 ralimdv y S k j z S F k z F j z < x k j F k y F j y < x
128 127 reximdv y S j Z k j z S F k z F j z < x j Z k j F k y F j y < x
129 128 ralimdv y S x + j Z k j z S F k z F j z < x x + j Z k j F k y F j y < x
130 129 impcom x + j Z k j z S F k z F j z < x y S x + j Z k j F k y F j y < x
131 130 adantll φ x + j Z k j z S F k z F j z < x y S x + j Z k j F k y F j y < x
132 fveq2 q = k n Z F n y q = n Z F n y k
133 132 fvoveq1d q = k n Z F n y q n Z F n y p = n Z F n y k n Z F n y p
134 133 breq1d q = k n Z F n y q n Z F n y p < r n Z F n y k n Z F n y p < r
135 134 cbvralvw q p n Z F n y q n Z F n y p < r k p n Z F n y k n Z F n y p < r
136 fveq2 p = j n Z F n y p = n Z F n y j
137 136 oveq2d p = j n Z F n y k n Z F n y p = n Z F n y k n Z F n y j
138 137 fveq2d p = j n Z F n y k n Z F n y p = n Z F n y k n Z F n y j
139 138 breq1d p = j n Z F n y k n Z F n y p < r n Z F n y k n Z F n y j < r
140 90 139 raleqbidv p = j k p n Z F n y k n Z F n y p < r k j n Z F n y k n Z F n y j < r
141 135 140 syl5bb p = j q p n Z F n y q n Z F n y p < r k j n Z F n y k n Z F n y j < r
142 141 cbvrexvw p Z q p n Z F n y q n Z F n y p < r j Z k j n Z F n y k n Z F n y j < r
143 fveq2 n = k F n = F k
144 143 fveq1d n = k F n y = F k y
145 eqid n Z F n y = n Z F n y
146 fvex F k y V
147 144 145 146 fvmpt k Z n Z F n y k = F k y
148 38 147 syl j Z k j n Z F n y k = F k y
149 fveq2 n = j F n = F j
150 149 fveq1d n = j F n y = F j y
151 fvex F j y V
152 150 145 151 fvmpt j Z n Z F n y j = F j y
153 152 adantr j Z k j n Z F n y j = F j y
154 148 153 oveq12d j Z k j n Z F n y k n Z F n y j = F k y F j y
155 154 fveq2d j Z k j n Z F n y k n Z F n y j = F k y F j y
156 155 breq1d j Z k j n Z F n y k n Z F n y j < r F k y F j y < r
157 156 ralbidva j Z k j n Z F n y k n Z F n y j < r k j F k y F j y < r
158 157 rexbiia j Z k j n Z F n y k n Z F n y j < r j Z k j F k y F j y < r
159 142 158 bitri p Z q p n Z F n y q n Z F n y p < r j Z k j F k y F j y < r
160 breq2 r = x F k y F j y < r F k y F j y < x
161 160 ralbidv r = x k j F k y F j y < r k j F k y F j y < x
162 161 rexbidv r = x j Z k j F k y F j y < r j Z k j F k y F j y < x
163 159 162 syl5bb r = x p Z q p n Z F n y q n Z F n y p < r j Z k j F k y F j y < x
164 163 cbvralvw r + p Z q p n Z F n y q n Z F n y p < r x + j Z k j F k y F j y < x
165 131 164 sylibr φ x + j Z k j z S F k z F j z < x y S r + p Z q p n Z F n y q n Z F n y p < r
166 1 fvexi Z V
167 166 mptex n Z F n y V
168 167 a1i φ x + j Z k j z S F k z F j z < x y S n Z F n y V
169 1 120 165 168 caucvg φ x + j Z k j z S F k z F j z < x y S n Z F n y dom
170 169 ralrimiva φ x + j Z k j z S F k z F j z < x y S n Z F n y dom
171 170 ad2antrr φ x + j Z k j z S F k z F j z < x r + q Z y S n Z F n y dom
172 fveq2 y = w F n y = F n w
173 172 mpteq2dv y = w n Z F n y = n Z F n w
174 173 eleq1d y = w n Z F n y dom n Z F n w dom
175 174 rspccva y S n Z F n y dom w S n Z F n w dom
176 171 175 sylan φ x + j Z k j z S F k z F j z < x r + q Z w S n Z F n w dom
177 climdm n Z F n w dom n Z F n w n Z F n w
178 176 177 sylib φ x + j Z k j z S F k z F j z < x r + q Z w S n Z F n w n Z F n w
179 98 101 103 112 178 climi2 φ x + j Z k j z S F k z F j z < x r + q Z w S v q m v F m w n Z F n w < r 2
180 98 r19.29uz m q F q w F m w < r 2 v q m v F m w n Z F n w < r 2 v q m v F q w F m w < r 2 F m w n Z F n w < r 2
181 98 r19.2uz v q m v F q w F m w < r 2 F m w n Z F n w < r 2 m q F q w F m w < r 2 F m w n Z F n w < r 2
182 180 181 syl m q F q w F m w < r 2 v q m v F m w n Z F n w < r 2 m q F q w F m w < r 2 F m w n Z F n w < r 2
183 4 ad2antrr φ x + j Z k j z S F k z F j z < x r + F : Z S
184 183 ffvelrnda φ x + j Z k j z S F k z F j z < x r + q Z F q S
185 elmapi F q S F q : S
186 184 185 syl φ x + j Z k j z S F k z F j z < x r + q Z F q : S
187 186 ffvelrnda φ x + j Z k j z S F k z F j z < x r + q Z w S F q w
188 187 adantr φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w
189 climcl n Z F n w n Z F n w n Z F n w
190 178 189 syl φ x + j Z k j z S F k z F j z < x r + q Z w S n Z F n w
191 190 adantr φ x + j Z k j z S F k z F j z < x r + q Z w S m q n Z F n w
192 4 ad5antr φ x + j Z k j z S F k z F j z < x r + q Z w S m q F : Z S
193 192 106 ffvelrnd φ x + j Z k j z S F k z F j z < x r + q Z w S m q F m S
194 elmapi F m S F m : S
195 193 194 syl φ x + j Z k j z S F k z F j z < x r + q Z w S m q F m : S
196 simplr φ x + j Z k j z S F k z F j z < x r + q Z w S m q w S
197 195 196 ffvelrnd φ x + j Z k j z S F k z F j z < x r + q Z w S m q F m w
198 rpre r + r
199 198 ad4antlr φ x + j Z k j z S F k z F j z < x r + q Z w S m q r
200 abs3lem F q w n Z F n w F m w r F q w F m w < r 2 F m w n Z F n w < r 2 F q w n Z F n w < r
201 188 191 197 199 200 syl22anc φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w F m w < r 2 F m w n Z F n w < r 2 F q w n Z F n w < r
202 201 rexlimdva φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w F m w < r 2 F m w n Z F n w < r 2 F q w n Z F n w < r
203 182 202 syl5 φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w F m w < r 2 v q m v F m w n Z F n w < r 2 F q w n Z F n w < r
204 179 203 mpan2d φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w F m w < r 2 F q w n Z F n w < r
205 204 ralimdva φ x + j Z k j z S F k z F j z < x r + q Z w S m q F q w F m w < r 2 w S F q w n Z F n w < r
206 97 205 sylan2 φ x + j Z k j z S F k z F j z < x r + p Z q p w S m q F q w F m w < r 2 w S F q w n Z F n w < r
207 206 anassrs φ x + j Z k j z S F k z F j z < x r + p Z q p w S m q F q w F m w < r 2 w S F q w n Z F n w < r
208 207 ralimdva φ x + j Z k j z S F k z F j z < x r + p Z q p w S m q F q w F m w < r 2 q p w S F q w n Z F n w < r
209 208 reximdva φ x + j Z k j z S F k z F j z < x r + p Z q p w S m q F q w F m w < r 2 p Z q p w S F q w n Z F n w < r
210 96 209 mpd φ x + j Z k j z S F k z F j z < x r + p Z q p w S F q w n Z F n w < r
211 210 ralrimiva φ x + j Z k j z S F k z F j z < x r + p Z q p w S F q w n Z F n w < r
212 2 adantr φ x + j Z k j z S F k z F j z < x M
213 eqidd φ x + j Z k j z S F k z F j z < x q Z w S F q w = F q w
214 173 fveq2d y = w n Z F n y = n Z F n w
215 eqid y S n Z F n y = y S n Z F n y
216 fvex n Z F n w V
217 214 215 216 fvmpt w S y S n Z F n y w = n Z F n w
218 217 adantl φ x + j Z k j z S F k z F j z < x w S y S n Z F n y w = n Z F n w
219 climdm n Z F n y dom n Z F n y n Z F n y
220 169 219 sylib φ x + j Z k j z S F k z F j z < x y S n Z F n y n Z F n y
221 climcl n Z F n y n Z F n y n Z F n y
222 220 221 syl φ x + j Z k j z S F k z F j z < x y S n Z F n y
223 222 fmpttd φ x + j Z k j z S F k z F j z < x y S n Z F n y : S
224 3 adantr φ x + j Z k j z S F k z F j z < x S V
225 1 212 113 213 218 223 224 ulm2 φ x + j Z k j z S F k z F j z < x F u S y S n Z F n y r + p Z q p w S F q w n Z F n w < r
226 211 225 mpbird φ x + j Z k j z S F k z F j z < x F u S y S n Z F n y
227 releldm Rel u S F u S y S n Z F n y F dom u S
228 65 226 227 sylancr φ x + j Z k j z S F k z F j z < x F dom u S
229 228 ex φ x + j Z k j z S F k z F j z < x F dom u S
230 64 229 impbid φ F dom u S x + j Z k j z S F k z F j z < x