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 fld
divcn.k K = J 𝑡 0
Assertion divcn ÷ J × t K Cn J

Proof

Step Hyp Ref Expression
1 mpomulcn.j J = TopOpen fld
2 divcn.k K = J 𝑡 0
3 df-div ÷ = x , y 0 ι z | y z = x
4 eldifsn y 0 y y 0
5 divval x y y 0 x y = ι z | y z = x
6 divrec x y y 0 x y = x 1 y
7 5 6 eqtr3d x y y 0 ι z | y z = x = x 1 y
8 7 3expb x y y 0 ι z | y z = x = x 1 y
9 4 8 sylan2b x y 0 ι z | y z = x = x 1 y
10 9 mpoeq3ia x , y 0 ι z | y z = x = x , y 0 x 1 y
11 3 10 eqtri ÷ = x , y 0 x 1 y
12 1 cnfldtopon J TopOn
13 12 a1i J TopOn
14 difss 0
15 resttopon J TopOn 0 J 𝑡 0 TopOn 0
16 13 14 15 sylancl J 𝑡 0 TopOn 0
17 2 16 eqeltrid K TopOn 0
18 13 17 cnmpt1st x , y 0 x J × t K Cn J
19 13 17 cnmpt2nd x , y 0 y J × t K Cn K
20 eqid z 0 1 z = z 0 1 z
21 eldifi z 0 z
22 eldifsni z 0 z 0
23 21 22 reccld z 0 1 z
24 20 23 fmpti z 0 1 z : 0
25 eqid if 1 x w 1 x w x 2 = if 1 x w 1 x w x 2
26 25 reccn2 x 0 w + a + y 0 y x < a 1 y 1 x < w
27 ovres x 0 y 0 x abs 0 × 0 y = x abs y
28 eldifi x 0 x
29 eldifi y 0 y
30 eqid abs = abs
31 30 cnmetdval x y x abs y = x y
32 abssub x y x y = y x
33 31 32 eqtrd x y x abs y = y x
34 28 29 33 syl2an x 0 y 0 x abs y = y x
35 27 34 eqtrd x 0 y 0 x abs 0 × 0 y = y x
36 35 breq1d x 0 y 0 x abs 0 × 0 y < a y x < a
37 oveq2 z = x 1 z = 1 x
38 ovex 1 x V
39 37 20 38 fvmpt x 0 z 0 1 z x = 1 x
40 oveq2 z = y 1 z = 1 y
41 ovex 1 y V
42 40 20 41 fvmpt y 0 z 0 1 z y = 1 y
43 39 42 oveqan12d x 0 y 0 z 0 1 z x abs z 0 1 z y = 1 x abs 1 y
44 eldifsni x 0 x 0
45 28 44 reccld x 0 1 x
46 eldifsni y 0 y 0
47 29 46 reccld y 0 1 y
48 30 cnmetdval 1 x 1 y 1 x abs 1 y = 1 x 1 y
49 abssub 1 x 1 y 1 x 1 y = 1 y 1 x
50 48 49 eqtrd 1 x 1 y 1 x abs 1 y = 1 y 1 x
51 45 47 50 syl2an x 0 y 0 1 x abs 1 y = 1 y 1 x
52 43 51 eqtrd x 0 y 0 z 0 1 z x abs z 0 1 z y = 1 y 1 x
53 52 breq1d x 0 y 0 z 0 1 z x abs z 0 1 z y < w 1 y 1 x < w
54 36 53 imbi12d x 0 y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w y x < a 1 y 1 x < w
55 54 ralbidva x 0 y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w y 0 y x < a 1 y 1 x < w
56 55 rexbidv x 0 a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w a + y 0 y x < a 1 y 1 x < w
57 56 adantr x 0 w + a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w a + y 0 y x < a 1 y 1 x < w
58 26 57 mpbird x 0 w + a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w
59 58 rgen2 x 0 w + a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w
60 cnxmet abs ∞Met
61 xmetres2 abs ∞Met 0 abs 0 × 0 ∞Met 0
62 60 14 61 mp2an abs 0 × 0 ∞Met 0
63 eqid abs 0 × 0 = abs 0 × 0
64 1 cnfldtopn J = MetOpen abs
65 eqid MetOpen abs 0 × 0 = MetOpen abs 0 × 0
66 63 64 65 metrest abs ∞Met 0 J 𝑡 0 = MetOpen abs 0 × 0
67 60 14 66 mp2an J 𝑡 0 = MetOpen abs 0 × 0
68 2 67 eqtri K = MetOpen abs 0 × 0
69 68 64 metcn abs 0 × 0 ∞Met 0 abs ∞Met z 0 1 z K Cn J z 0 1 z : 0 x 0 w + a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w
70 62 60 69 mp2an z 0 1 z K Cn J z 0 1 z : 0 x 0 w + a + y 0 x abs 0 × 0 y < a z 0 1 z x abs z 0 1 z y < w
71 24 59 70 mpbir2an z 0 1 z K Cn J
72 71 a1i z 0 1 z K Cn J
73 13 17 19 17 72 40 cnmpt21 x , y 0 1 y J × t K Cn J
74 1 mpomulcn u , v u v J × t J Cn J
75 74 a1i u , v u v J × t J Cn J
76 oveq12 u = x v = 1 y u v = x 1 y
77 13 17 18 73 13 13 75 76 cnmpt22 x , y 0 x 1 y J × t K Cn J
78 77 mptru x , y 0 x 1 y J × t K Cn J
79 11 78 eqeltri ÷ J × t K Cn J