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) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypotheses mpomulcn.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 mpomulcn.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 eldifi 
 |-  ( z e. ( CC \ { 0 } ) -> z e. CC )
22 eldifsni 
 |-  ( z e. ( CC \ { 0 } ) -> z =/= 0 )
23 21 22 reccld 
 |-  ( 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. w ) , 1 , ( ( abs ` x ) x. w ) ) x. ( ( abs ` x ) / 2 ) ) = ( if ( 1 <_ ( ( abs ` x ) x. w ) , 1 , ( ( abs ` x ) x. w ) ) x. ( ( abs ` x ) / 2 ) )
26 25 reccn2 
 |-  ( ( x e. ( CC \ { 0 } ) /\ w e. RR+ ) -> E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( abs ` ( y - x ) ) < a -> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) )
27 ovres 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) = ( x ( abs o. - ) y ) )
28 eldifi 
 |-  ( x e. ( CC \ { 0 } ) -> x e. CC )
29 eldifi 
 |-  ( y e. ( CC \ { 0 } ) -> y e. CC )
30 eqid 
 |-  ( abs o. - ) = ( abs o. - )
31 30 cnmetdval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( abs o. - ) y ) = ( abs ` ( x - y ) ) )
32 abssub 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
33 31 32 eqtrd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( abs o. - ) y ) = ( abs ` ( y - x ) ) )
34 28 29 33 syl2an 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x ( abs o. - ) y ) = ( abs ` ( y - x ) ) )
35 27 34 eqtrd 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) = ( abs ` ( y - x ) ) )
36 35 breq1d 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a <-> ( abs ` ( y - x ) ) < a ) )
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 = y -> ( 1 / z ) = ( 1 / y ) )
41 ovex 
 |-  ( 1 / y ) e. _V
42 40 20 41 fvmpt 
 |-  ( y e. ( CC \ { 0 } ) -> ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) = ( 1 / y ) )
43 39 42 oveqan12d 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) = ( ( 1 / x ) ( abs o. - ) ( 1 / y ) ) )
44 eldifsni 
 |-  ( x e. ( CC \ { 0 } ) -> x =/= 0 )
45 28 44 reccld 
 |-  ( x e. ( CC \ { 0 } ) -> ( 1 / x ) e. CC )
46 eldifsni 
 |-  ( y e. ( CC \ { 0 } ) -> y =/= 0 )
47 29 46 reccld 
 |-  ( y e. ( CC \ { 0 } ) -> ( 1 / y ) e. CC )
48 30 cnmetdval 
 |-  ( ( ( 1 / x ) e. CC /\ ( 1 / y ) e. CC ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / y ) ) = ( abs ` ( ( 1 / x ) - ( 1 / y ) ) ) )
49 abssub 
 |-  ( ( ( 1 / x ) e. CC /\ ( 1 / y ) e. CC ) -> ( abs ` ( ( 1 / x ) - ( 1 / y ) ) ) = ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) )
50 48 49 eqtrd 
 |-  ( ( ( 1 / x ) e. CC /\ ( 1 / y ) e. CC ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / y ) ) = ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) )
51 45 47 50 syl2an 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( 1 / x ) ( abs o. - ) ( 1 / y ) ) = ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) )
52 43 51 eqtrd 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) = ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) )
53 52 breq1d 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w <-> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) )
54 36 53 imbi12d 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) <-> ( ( abs ` ( y - x ) ) < a -> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) ) )
55 54 ralbidva 
 |-  ( x e. ( CC \ { 0 } ) -> ( A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) <-> A. y e. ( CC \ { 0 } ) ( ( abs ` ( y - x ) ) < a -> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) ) )
56 55 rexbidv 
 |-  ( x e. ( CC \ { 0 } ) -> ( E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) <-> E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( abs ` ( y - x ) ) < a -> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) ) )
57 56 adantr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ w e. RR+ ) -> ( E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) <-> E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( abs ` ( y - x ) ) < a -> ( abs ` ( ( 1 / y ) - ( 1 / x ) ) ) < w ) ) )
58 26 57 mpbird 
 |-  ( ( x e. ( CC \ { 0 } ) /\ w e. RR+ ) -> E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) )
59 58 rgen2 
 |-  A. x e. ( CC \ { 0 } ) A. w e. RR+ E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w )
60 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
61 xmetres2 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. ( *Met ` ( CC \ { 0 } ) ) )
62 60 14 61 mp2an 
 |-  ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) e. ( *Met ` ( CC \ { 0 } ) )
63 eqid 
 |-  ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) = ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) )
64 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
65 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) )
66 63 64 65 metrest 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( J |`t ( CC \ { 0 } ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) ) )
67 60 14 66 mp2an 
 |-  ( J |`t ( CC \ { 0 } ) ) = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) )
68 2 67 eqtri 
 |-  K = ( MetOpen ` ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) )
69 68 64 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. w e. RR+ E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) ) ) )
70 62 60 69 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. w e. RR+ E. a e. RR+ A. y e. ( CC \ { 0 } ) ( ( x ( ( abs o. - ) |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) < a -> ( ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` x ) ( abs o. - ) ( ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) ` y ) ) < w ) ) )
71 24 59 70 mpbir2an 
 |-  ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J )
72 71 a1i 
 |-  ( T. -> ( z e. ( CC \ { 0 } ) |-> ( 1 / z ) ) e. ( K Cn J ) )
73 13 17 19 17 72 40 cnmpt21 
 |-  ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> ( 1 / y ) ) e. ( ( J tX K ) Cn J ) )
74 1 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J )
75 74 a1i 
 |-  ( T. -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J ) )
76 oveq12 
 |-  ( ( u = x /\ v = ( 1 / y ) ) -> ( u x. v ) = ( x x. ( 1 / y ) ) )
77 13 17 18 73 13 13 75 76 cnmpt22 
 |-  ( T. -> ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) e. ( ( J tX K ) Cn J ) )
78 77 mptru 
 |-  ( x e. CC , y e. ( CC \ { 0 } ) |-> ( x x. ( 1 / y ) ) ) e. ( ( J tX K ) Cn J )
79 11 78 eqeltri 
 |-  / e. ( ( J tX K ) Cn J )