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