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⁡ℂfld
divcn.k ⊢K=J↾𝑡ℂ∖0
Assertion divcn ⊢÷∈J×tKCnJ

Proof

Step Hyp Ref Expression
1 addcn.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 eldifsn ⊢z∈ℂ∖0↔z∈ℂ∧z≠0
22 reccl ⊢z∈ℂ∧z≠0→1z∈ℂ
23 21 22 sylbi ⊢z∈ℂ∖0→1z∈ℂ
24 20 23 fmpti ⊢z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ
25 eqid ⊢if1≤x⁢y1x⁢y⁢x2=if1≤x⁢y1x⁢y⁢x2
26 25 reccn2 ⊢x∈ℂ∖0∧y∈ℝ+→∃u∈ℝ+∀w∈ℂ∖0w−x<u→1w−1x<y
27 ovres ⊢x∈ℂ∖0∧w∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0w=xabs∘−w
28 eldifi ⊢x∈ℂ∖0→x∈ℂ
29 eldifi ⊢w∈ℂ∖0→w∈ℂ
30 eqid ⊢abs∘−=abs∘−
31 30 cnmetdval ⊢x∈ℂ∧w∈ℂ→xabs∘−w=x−w
32 abssub ⊢x∈ℂ∧w∈ℂ→x−w=w−x
33 31 32 eqtrd ⊢x∈ℂ∧w∈ℂ→xabs∘−w=w−x
34 28 29 33 syl2an ⊢x∈ℂ∖0∧w∈ℂ∖0→xabs∘−w=w−x
35 27 34 eqtrd ⊢x∈ℂ∖0∧w∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0w=w−x
36 35 breq1d ⊢x∈ℂ∖0∧w∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0w<u↔w−x<u
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=w→1z=1w
41 ovex ⊢1w∈V
42 40 20 41 fvmpt ⊢w∈ℂ∖0→z∈ℂ∖0⟼1z⁡w=1w
43 39 42 oveqan12d ⊢x∈ℂ∖0∧w∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w=1xabs∘−1w
44 eldifsn ⊢x∈ℂ∖0↔x∈ℂ∧x≠0
45 reccl ⊢x∈ℂ∧x≠0→1x∈ℂ
46 44 45 sylbi ⊢x∈ℂ∖0→1x∈ℂ
47 eldifsn ⊢w∈ℂ∖0↔w∈ℂ∧w≠0
48 reccl ⊢w∈ℂ∧w≠0→1w∈ℂ
49 47 48 sylbi ⊢w∈ℂ∖0→1w∈ℂ
50 30 cnmetdval ⊢1x∈ℂ∧1w∈ℂ→1xabs∘−1w=1x−1w
51 abssub ⊢1x∈ℂ∧1w∈ℂ→1x−1w=1w−1x
52 50 51 eqtrd ⊢1x∈ℂ∧1w∈ℂ→1xabs∘−1w=1w−1x
53 46 49 52 syl2an ⊢x∈ℂ∖0∧w∈ℂ∖0→1xabs∘−1w=1w−1x
54 43 53 eqtrd ⊢x∈ℂ∖0∧w∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w=1w−1x
55 54 breq1d ⊢x∈ℂ∖0∧w∈ℂ∖0→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y↔1w−1x<y
56 36 55 imbi12d ⊢x∈ℂ∖0∧w∈ℂ∖0→xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y↔w−x<u→1w−1x<y
57 56 ralbidva ⊢x∈ℂ∖0→∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y↔∀w∈ℂ∖0w−x<u→1w−1x<y
58 57 rexbidv ⊢x∈ℂ∖0→∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y↔∃u∈ℝ+∀w∈ℂ∖0w−x<u→1w−1x<y
59 58 adantr ⊢x∈ℂ∖0∧y∈ℝ+→∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y↔∃u∈ℝ+∀w∈ℂ∖0w−x<u→1w−1x<y
60 26 59 mpbird ⊢x∈ℂ∖0∧y∈ℝ+→∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y
61 60 rgen2 ⊢∀x∈ℂ∖0∀y∈ℝ+∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y
62 cnxmet ⊢abs∘−∈∞Met⁡ℂ
63 xmetres2 ⊢abs∘−∈∞Met⁡ℂ∧ℂ∖0⊆ℂ→abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0
64 62 14 63 mp2an ⊢abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0
65 eqid ⊢abs∘−↾ℂ∖0×ℂ∖0=abs∘−↾ℂ∖0×ℂ∖0
66 1 cnfldtopn ⊢J=MetOpen⁡abs∘−
67 eqid ⊢MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
68 65 66 67 metrest ⊢abs∘−∈∞Met⁡ℂ∧ℂ∖0⊆ℂ→J↾𝑡ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
69 62 14 68 mp2an ⊢J↾𝑡ℂ∖0=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
70 2 69 eqtri ⊢K=MetOpen⁡abs∘−↾ℂ∖0×ℂ∖0
71 70 66 metcn ⊢abs∘−↾ℂ∖0×ℂ∖0∈∞Met⁡ℂ∖0∧abs∘−∈∞Met⁡ℂ→z∈ℂ∖0⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀y∈ℝ+∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y
72 64 62 71 mp2an ⊢z∈ℂ∖0⟼1z∈KCnJ↔z∈ℂ∖0⟼1z:ℂ∖0⟶ℂ∧∀x∈ℂ∖0∀y∈ℝ+∃u∈ℝ+∀w∈ℂ∖0xabs∘−↾ℂ∖0×ℂ∖0w<u→z∈ℂ∖0⟼1z⁡xabs∘−z∈ℂ∖0⟼1z⁡w<y
73 24 61 72 mpbir2an ⊢z∈ℂ∖0⟼1z∈KCnJ
74 73 a1i ⊢⊤→z∈ℂ∖0⟼1z∈KCnJ
75 oveq2 ⊢z=y→1z=1y
76 13 17 19 17 74 75 cnmpt21 ⊢⊤→x∈ℂ,y∈ℂ∖0⟼1y∈J×tKCnJ
77 1 mulcn ⊢×∈J×tJCnJ
78 77 a1i ⊢⊤→×∈J×tJCnJ
79 13 17 18 76 78 cnmpt22f ⊢⊤→x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
80 79 mptru ⊢x∈ℂ,y∈ℂ∖0⟼x⁢1y∈J×tKCnJ
81 11 80 eqeltri ⊢÷∈J×tKCnJ