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×tKCnJ

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→xy=ιz∈ℂ|y⁢z=x
6 divrec ⊢x∈ℂ∧y∈ℂ∧y≠0→xy=x⁢1y
7 5 6 eqtr3d ⊢x∈ℂ∧y∈ℂ∧y≠0→ιz∈ℂ|y⁢z=x=x⁢1y
8 7 3expb ⊢x∈ℂ∧y∈ℂ∧y≠0→ιz∈ℂ|y⁢z=x=x⁢1y
9 4 8 sylan2b ⊢x∈ℂ∧y∈ℂ∖0→ιz∈ℂ|y⁢z=x=x⁢1y
10 9 mpoeq3ia ⊢x∈ℂ,y∈ℂ∖0⟼ιz∈ℂ|y⁢z=x=x∈ℂ,y∈ℂ∖0⟼x⁢1y
11 3 10 eqtri ⊢÷=x∈ℂ,y∈ℂ∖0⟼x⁢1y
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×tKCnJ
19 13 17 cnmpt2nd ⊢⊤→x∈ℂ,y∈ℂ∖0⟼y∈J×tKCnK
20 eqid ⊢z∈ℂ∖0⟼1z=z∈ℂ∖0⟼1z
21 eldifi ⊢z∈ℂ∖0→z∈ℂ
22 eldifsni ⊢z∈ℂ∖0→z≠0
23 21 22 reccld ⊢z∈ℂ∖0→1z∈ℂ
24 20 23 fmpti ⊢z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ
25 eqid ⊢if1≤x⁢w1x⁢w⁢x2=if1≤x⁢w1x⁢w⁢x2
26 25 reccn2 ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
27 ovres ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y=xabs∘−y
28 eldifi ⊢x∈ℂ∖0→x∈ℂ
29 eldifi ⊢y∈ℂ∖0→y∈ℂ
30 eqid ⊢abs∘−=abs∘−
31 30 cnmetdval ⊢x∈ℂ∧y∈ℂ→xabs∘−y=x−y
32 abssub ⊢x∈ℂ∧y∈ℂ→x−y=y−x
33 31 32 eqtrd ⊢x∈ℂ∧y∈ℂ→xabs∘−y=y−x
34 28 29 33 syl2an ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−y=y−x
35 27 34 eqtrd ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y=y−x
36 35 breq1d ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y<a↔y−x<a
37 oveq2 ⊢z=x→1z=1x
38 ovex ⊢1x∈V
39 37 20 38 fvmpt ⊢x∈ℂ∖0→z∈ℂ∖0⟼1z⁡x=1x
40 oveq2 ⊢z=y→1z=1y
41 ovex ⊢1y∈V
42 40 20 41 fvmpt ⊢y∈ℂ∖0→z∈ℂ∖0⟼1z⁡y=1y
43 39 42 oveqan12d ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y=1xabs∘−1y
44 eldifsni ⊢x∈ℂ∖0→x≠0
45 28 44 reccld ⊢x∈ℂ∖0→1x∈ℂ
46 eldifsni ⊢y∈ℂ∖0→y≠0
47 29 46 reccld ⊢y∈ℂ∖0→1y∈ℂ
48 30 cnmetdval ⊢1x∈ℂ∧1y∈ℂ→1xabs∘−1y=1x−1y
49 abssub ⊢1x∈ℂ∧1y∈ℂ→1x−1y=1y−1x
50 48 49 eqtrd ⊢1x∈ℂ∧1y∈ℂ→1xabs∘−1y=1y−1x
51 45 47 50 syl2an ⊢x∈ℂ∖0∧y∈ℂ∖0→1xabs∘−1y=1y−1x
52 43 51 eqtrd ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y=1y−1x
53 52 breq1d ⊢x∈ℂ∖0∧y∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔1y−1x<w
54 36 53 imbi12d ⊢x∈ℂ∖0∧y∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔y−x<a→1y−1x<w
55 54 ralbidva ⊢x∈ℂ∖0→∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∀y∈ℂ∖0y−x<a→1y−1x<w
56 55 rexbidv ⊢x∈ℂ∖0→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
57 56 adantr ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w↔∃a∈ℝ+∀y∈ℂ∖0y−x<a→1y−1x<w
58 26 57 mpbird ⊢x∈ℂ∖0∧w∈ℝ+→∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
59 58 rgen2 ⊢∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡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⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
70 62 60 69 mp2an ⊢z∈ℂ∖0⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀w∈ℝ+∃a∈ℝ+∀y∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0y<a→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡y<w
71 24 59 70 mpbir2an ⊢z∈ℂ∖0⟼1z∈KCnJ
72 71 a1i ⊢⊤→z∈ℂ∖0⟼1z∈KCnJ
73 13 17 19 17 72 40 cnmpt21 ⊢⊤→x∈ℂ,y∈ℂ∖0⟼1y∈J×tKCnJ
74 1 mpomulcn ⊢u∈ℂ,v∈ℂ⟼u⁢v∈J×tJCnJ
75 74 a1i ⊢⊤→u∈ℂ,v∈ℂ⟼u⁢v∈J×tJCnJ
76 oveq12 ⊢u=x∧v=1y→u⁢v=x⁢1y
77 13 17 18 73 13 13 75 76 cnmpt22 ⊢⊤→x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
78 77 mptru ⊢x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
79 11 78 eqeltri ⊢÷∈J×tKCnJ