Step |
Hyp |
Ref |
Expression |
0 |
|
culm |
|- ~~>u |
1 |
|
vs |
|- s |
2 |
|
cvv |
|- _V |
3 |
|
vf |
|- f |
4 |
|
vy |
|- y |
5 |
|
vn |
|- n |
6 |
|
cz |
|- ZZ |
7 |
3
|
cv |
|- f |
8 |
|
cuz |
|- ZZ>= |
9 |
5
|
cv |
|- n |
10 |
9 8
|
cfv |
|- ( ZZ>= ` n ) |
11 |
|
cc |
|- CC |
12 |
|
cmap |
|- ^m |
13 |
1
|
cv |
|- s |
14 |
11 13 12
|
co |
|- ( CC ^m s ) |
15 |
10 14 7
|
wf |
|- f : ( ZZ>= ` n ) --> ( CC ^m s ) |
16 |
4
|
cv |
|- y |
17 |
13 11 16
|
wf |
|- y : s --> CC |
18 |
|
vx |
|- x |
19 |
|
crp |
|- RR+ |
20 |
|
vj |
|- j |
21 |
|
vk |
|- k |
22 |
20
|
cv |
|- j |
23 |
22 8
|
cfv |
|- ( ZZ>= ` j ) |
24 |
|
vz |
|- z |
25 |
|
cabs |
|- abs |
26 |
21
|
cv |
|- k |
27 |
26 7
|
cfv |
|- ( f ` k ) |
28 |
24
|
cv |
|- z |
29 |
28 27
|
cfv |
|- ( ( f ` k ) ` z ) |
30 |
|
cmin |
|- - |
31 |
28 16
|
cfv |
|- ( y ` z ) |
32 |
29 31 30
|
co |
|- ( ( ( f ` k ) ` z ) - ( y ` z ) ) |
33 |
32 25
|
cfv |
|- ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) |
34 |
|
clt |
|- < |
35 |
18
|
cv |
|- x |
36 |
33 35 34
|
wbr |
|- ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x |
37 |
36 24 13
|
wral |
|- A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x |
38 |
37 21 23
|
wral |
|- A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x |
39 |
38 20 10
|
wrex |
|- E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x |
40 |
39 18 19
|
wral |
|- A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x |
41 |
15 17 40
|
w3a |
|- ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) |
42 |
41 5 6
|
wrex |
|- E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) |
43 |
42 3 4
|
copab |
|- { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } |
44 |
1 2 43
|
cmpt |
|- ( s e. _V |-> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } ) |
45 |
0 44
|
wceq |
|- ~~>u = ( s e. _V |-> { <. f , y >. | E. n e. ZZ ( f : ( ZZ>= ` n ) --> ( CC ^m s ) /\ y : s --> CC /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) A. z e. s ( abs ` ( ( ( f ` k ) ` z ) - ( y ` z ) ) ) < x ) } ) |