Step |
Hyp |
Ref |
Expression |
0 |
|
cli |
|- ~~> |
1 |
|
vf |
|- f |
2 |
|
vy |
|- y |
3 |
2
|
cv |
|- y |
4 |
|
cc |
|- CC |
5 |
3 4
|
wcel |
|- y e. CC |
6 |
|
vx |
|- x |
7 |
|
crp |
|- RR+ |
8 |
|
vj |
|- j |
9 |
|
cz |
|- ZZ |
10 |
|
vk |
|- k |
11 |
|
cuz |
|- ZZ>= |
12 |
8
|
cv |
|- j |
13 |
12 11
|
cfv |
|- ( ZZ>= ` j ) |
14 |
1
|
cv |
|- f |
15 |
10
|
cv |
|- k |
16 |
15 14
|
cfv |
|- ( f ` k ) |
17 |
16 4
|
wcel |
|- ( f ` k ) e. CC |
18 |
|
cabs |
|- abs |
19 |
|
cmin |
|- - |
20 |
16 3 19
|
co |
|- ( ( f ` k ) - y ) |
21 |
20 18
|
cfv |
|- ( abs ` ( ( f ` k ) - y ) ) |
22 |
|
clt |
|- < |
23 |
6
|
cv |
|- x |
24 |
21 23 22
|
wbr |
|- ( abs ` ( ( f ` k ) - y ) ) < x |
25 |
17 24
|
wa |
|- ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) |
26 |
25 10 13
|
wral |
|- A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) |
27 |
26 8 9
|
wrex |
|- E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) |
28 |
27 6 7
|
wral |
|- A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) |
29 |
5 28
|
wa |
|- ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) |
30 |
29 1 2
|
copab |
|- { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) } |
31 |
0 30
|
wceq |
|- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) } |