Metamath Proof Explorer

Theorem divcn

Description: Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses addcn.j 
|- J = ( TopOpen ` CCfld )
divcn.k 
|- K = ( J |`t ( CC \ { 0 } ) )
Assertion divcn 
|- / e. ( ( J tX K ) Cn J )

Proof

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 )