Step |
Hyp |
Ref |
Expression |
0 |
|
ccncf |
|- -cn-> |
1 |
|
va |
|- a |
2 |
|
cc |
|- CC |
3 |
2
|
cpw |
|- ~P CC |
4 |
|
vb |
|- b |
5 |
|
vf |
|- f |
6 |
4
|
cv |
|- b |
7 |
|
cmap |
|- ^m |
8 |
1
|
cv |
|- a |
9 |
6 8 7
|
co |
|- ( b ^m a ) |
10 |
|
vx |
|- x |
11 |
|
ve |
|- e |
12 |
|
crp |
|- RR+ |
13 |
|
vd |
|- d |
14 |
|
vy |
|- y |
15 |
|
cabs |
|- abs |
16 |
10
|
cv |
|- x |
17 |
|
cmin |
|- - |
18 |
14
|
cv |
|- y |
19 |
16 18 17
|
co |
|- ( x - y ) |
20 |
19 15
|
cfv |
|- ( abs ` ( x - y ) ) |
21 |
|
clt |
|- < |
22 |
13
|
cv |
|- d |
23 |
20 22 21
|
wbr |
|- ( abs ` ( x - y ) ) < d |
24 |
5
|
cv |
|- f |
25 |
16 24
|
cfv |
|- ( f ` x ) |
26 |
18 24
|
cfv |
|- ( f ` y ) |
27 |
25 26 17
|
co |
|- ( ( f ` x ) - ( f ` y ) ) |
28 |
27 15
|
cfv |
|- ( abs ` ( ( f ` x ) - ( f ` y ) ) ) |
29 |
11
|
cv |
|- e |
30 |
28 29 21
|
wbr |
|- ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e |
31 |
23 30
|
wi |
|- ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) |
32 |
31 14 8
|
wral |
|- A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) |
33 |
32 13 12
|
wrex |
|- E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) |
34 |
33 11 12
|
wral |
|- A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) |
35 |
34 10 8
|
wral |
|- A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) |
36 |
35 5 9
|
crab |
|- { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } |
37 |
1 4 3 3 36
|
cmpo |
|- ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } ) |
38 |
0 37
|
wceq |
|- -cn-> = ( a e. ~P CC , b e. ~P CC |-> { f e. ( b ^m a ) | A. x e. a A. e e. RR+ E. d e. RR+ A. y e. a ( ( abs ` ( x - y ) ) < d -> ( abs ` ( ( f ` x ) - ( f ` y ) ) ) < e ) } ) |