Step |
Hyp |
Ref |
Expression |
1 |
|
addcn.j |
|- J = ( TopOpen ` CCfld ) |
2 |
|
divcn.k |
|- K = ( J |`t ( CC \ { 0 } ) ) |
3 |
|
df-div |
|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) ) |
4 |
|
eldifsn |
|- ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) ) |
5 |
|
divval |
|- ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( x / y ) = ( iota_ z e. CC ( y x. z ) = x ) ) |
6 |
|
divrec |
|- ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( x / y ) = ( x x. ( 1 / y ) ) ) |
7 |
5 6
|
eqtr3d |
|- ( ( x e. CC /\ y e. CC /\ y =/= 0 ) -> ( iota_ z e. CC ( y x. z ) = x ) = ( x x. ( 1 / y ) ) ) |
8 |
7
|
3expb |
|- ( ( x e. CC /\ ( y e. CC /\ y =/= 0 ) ) -> ( iota_ z e. CC ( y x. z ) = x ) = ( x x. ( 1 / y ) ) ) |
9 |
4 8
|
sylan2b |
|- ( ( x e. CC /\ y e. ( CC \ { 0 } ) ) -> ( iota_ z e. CC ( y x. z ) = x ) = ( x x. ( 1 / y ) ) ) |
10 |
9
|
mpoeq3ia |
|- ( x e. CC , y e. ( CC \ { 0 } ) |-> ( iota_ z e. CC ( y x. z ) = x ) ) = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) |
11 |
3 10
|
eqtri |
|- / = ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) |
12 |
1
|
cnfldtopon |
|- J e. ( TopOn ` CC ) |
13 |
12
|
a1i |
|- ( T. -> J e. ( TopOn ` CC ) ) |
14 |
|
difss |
|- ( CC \ { 0 } ) C_ CC |
15 |
|
resttopon |
|- ( ( J e. ( TopOn ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( J |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) ) |
16 |
13 14 15
|
sylancl |
|- ( T. -> ( J |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) ) |
17 |
2 16
|
eqeltrid |
|- ( T. -> K e. ( TopOn ` ( CC \ { 0 } ) ) ) |
18 |
13 17
|
cnmpt1st |
|- ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> x ) e. ( ( J tX K ) Cn J ) ) |
19 |
13 17
|
cnmpt2nd |
|- ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> y ) e. ( ( J tX K ) Cn K ) ) |
20 |
|
eqid |
|- ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) = ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) |
21 |
|
eldifsn |
|- ( z e. ( CC \ { 0 } ) <-> ( z e. CC /\ z =/= 0 ) ) |
22 |
|
reccl |
|- ( ( z e. CC /\ z =/= 0 ) -> ( 1 / z ) e. CC ) |
23 |
21 22
|
sylbi |
|- ( z e. ( CC \ { 0 } ) -> ( 1 / z ) e. CC ) |
24 |
20 23
|
fmpti |
|- ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) : ( CC \ { 0 } ) --> CC |
25 |
|
eqid |
|- ( if ( 1 <_ ( ( abs ` x ) x. y ) , 1 , ( ( abs ` x ) x. y ) ) x. ( ( abs ` x ) / 2 ) ) = ( if ( 1 <_ ( ( abs ` x ) x. y ) , 1 , ( ( abs ` x ) x. y ) ) x. ( ( abs ` x ) / 2 ) ) |
26 |
25
|
reccn2 |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. RR+ ) -> E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( abs ` ( w - x ) ) < u -> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) |
27 |
|
ovres |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) = ( x ( abs o. - ) w ) ) |
28 |
|
eldifi |
|- ( x e. ( CC \ { 0 } ) -> x e. CC ) |
29 |
|
eldifi |
|- ( w e. ( CC \ { 0 } ) -> w e. CC ) |
30 |
|
eqid |
|- ( abs o. - ) = ( abs o. - ) |
31 |
30
|
cnmetdval |
|- ( ( x e. CC /\ w e. CC ) -> ( x ( abs o. - ) w ) = ( abs ` ( x - w ) ) ) |
32 |
|
abssub |
|- ( ( x e. CC /\ w e. CC ) -> ( abs ` ( x - w ) ) = ( abs ` ( w - x ) ) ) |
33 |
31 32
|
eqtrd |
|- ( ( x e. CC /\ w e. CC ) -> ( x ( abs o. - ) w ) = ( abs ` ( w - x ) ) ) |
34 |
28 29 33
|
syl2an |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( x ( abs o. - ) w ) = ( abs ` ( w - x ) ) ) |
35 |
27 34
|
eqtrd |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) = ( abs ` ( w - x ) ) ) |
36 |
35
|
breq1d |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u <-> ( abs ` ( w - x ) ) < u ) ) |
37 |
|
oveq2 |
|- ( z = x -> ( 1 / z ) = ( 1 / x ) ) |
38 |
|
ovex |
|- ( 1 / x ) e. _V |
39 |
37 20 38
|
fvmpt |
|- ( x e. ( CC \ { 0 } ) -> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) = ( 1 / x ) ) |
40 |
|
oveq2 |
|- ( z = w -> ( 1 / z ) = ( 1 / w ) ) |
41 |
|
ovex |
|- ( 1 / w ) e. _V |
42 |
40 20 41
|
fvmpt |
|- ( w e. ( CC \ { 0 } ) -> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) = ( 1 / w ) ) |
43 |
39 42
|
oveqan12d |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) = ( ( 1 / x ) ( abs o. - ) ( 1 / w ) ) ) |
44 |
|
eldifsn |
|- ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) ) |
45 |
|
reccl |
|- ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC ) |
46 |
44 45
|
sylbi |
|- ( x e. ( CC \ { 0 } ) -> ( 1 / x ) e. CC ) |
47 |
|
eldifsn |
|- ( w e. ( CC \ { 0 } ) <-> ( w e. CC /\ w =/= 0 ) ) |
48 |
|
reccl |
|- ( ( w e. CC /\ w =/= 0 ) -> ( 1 / w ) e. CC ) |
49 |
47 48
|
sylbi |
|- ( w e. ( CC \ { 0 } ) -> ( 1 / w ) e. CC ) |
50 |
30
|
cnmetdval |
|- ( ( ( 1 / x ) e. CC /\ ( 1 / w ) e. CC ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / w ) ) = ( abs ` ( ( 1 / x ) - ( 1 / w ) ) ) ) |
51 |
|
abssub |
|- ( ( ( 1 / x ) e. CC /\ ( 1 / w ) e. CC ) -> ( abs ` ( ( 1 / x ) - ( 1 / w ) ) ) = ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) ) |
52 |
50 51
|
eqtrd |
|- ( ( ( 1 / x ) e. CC /\ ( 1 / w ) e. CC ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / w ) ) = ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) ) |
53 |
46 49 52
|
syl2an |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / w ) ) = ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) ) |
54 |
43 53
|
eqtrd |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) = ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) ) |
55 |
54
|
breq1d |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y <-> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) |
56 |
36 55
|
imbi12d |
|- ( ( x e. ( CC \ { 0 } ) /\ w e. ( CC \ { 0 } ) ) -> ( ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) <-> ( ( abs ` ( w - x ) ) < u -> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) ) |
57 |
56
|
ralbidva |
|- ( x e. ( CC \ { 0 } ) -> ( A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) <-> A. w e. ( CC \ { 0 } ) ( ( abs ` ( w - x ) ) < u -> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) ) |
58 |
57
|
rexbidv |
|- ( x e. ( CC \ { 0 } ) -> ( E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) <-> E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( abs ` ( w - x ) ) < u -> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) ) |
59 |
58
|
adantr |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. RR+ ) -> ( E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) <-> E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( abs ` ( w - x ) ) < u -> ( abs ` ( ( 1 / w ) - ( 1 / x ) ) ) < y ) ) ) |
60 |
26 59
|
mpbird |
|- ( ( x e. ( CC \ { 0 } ) /\ y e. RR+ ) -> E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) ) |
61 |
60
|
rgen2 |
|- A. x e. ( CC \ { 0 } ) A. y e. RR+ E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) |
62 |
|
cnxmet |
|- ( abs o. - ) e. ( *Met ` CC ) |
63 |
|
xmetres2 |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. ( *Met ` ( CC \ { 0 } ) ) ) |
64 |
62 14 63
|
mp2an |
|- ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. ( *Met ` ( CC \ { 0 } ) ) |
65 |
|
eqid |
|- ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) = ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) |
66 |
1
|
cnfldtopn |
|- J = ( MetOpen ` ( abs o. - ) ) |
67 |
|
eqid |
|- ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) |
68 |
65 66 67
|
metrest |
|- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( J |`t ( CC \ { 0 } ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) ) |
69 |
62 14 68
|
mp2an |
|- ( J |`t ( CC \ { 0 } ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) |
70 |
2 69
|
eqtri |
|- K = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) |
71 |
70 66
|
metcn |
|- ( ( ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. ( *Met ` ( CC \ { 0 } ) ) /\ ( abs o. - ) e. ( *Met ` CC ) ) -> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J ) <-> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) : ( CC \ { 0 } ) --> CC /\ A. x e. ( CC \ { 0 } ) A. y e. RR+ E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) ) ) ) |
72 |
64 62 71
|
mp2an |
|- ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J ) <-> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) : ( CC \ { 0 } ) --> CC /\ A. x e. ( CC \ { 0 } ) A. y e. RR+ E. u e. RR+ A. w e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) w ) < u -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` w ) ) < y ) ) ) |
73 |
24 61 72
|
mpbir2an |
|- ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J ) |
74 |
73
|
a1i |
|- ( T. -> ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J ) ) |
75 |
|
oveq2 |
|- ( z = y -> ( 1 / z ) = ( 1 / y ) ) |
76 |
13 17 19 17 74 75
|
cnmpt21 |
|- ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) e. ( ( J tX K ) Cn J ) ) |
77 |
1
|
mulcn |
|- x. e. ( ( J tX J ) Cn J ) |
78 |
77
|
a1i |
|- ( T. -> x. e. ( ( J tX J ) Cn J ) ) |
79 |
13 17 18 76 78
|
cnmpt22f |
|- ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) e. ( ( J tX K ) Cn J ) ) |
80 |
79
|
mptru |
|- ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) e. ( ( J tX K ) Cn J ) |
81 |
11 80
|
eqeltri |
|- / e. ( ( J tX K ) Cn J ) |