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 )