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 × t K Cn J

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 → 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 eldifsn ⊢ z ∈ ℂ ∖ 0 ↔ z ∈ ℂ ∧ z ≠ 0
22 reccl ⊢ z ∈ ℂ ∧ z ≠ 0 → 1 z ∈ ℂ
23 21 22 sylbi ⊢ z ∈ ℂ ∖ 0 → 1 z ∈ ℂ
24 20 23 fmpti ⊢ z ∈ ℂ ∖ 0 ⟼ 1 z : ℂ ∖ 0 ⟶ ℂ
25 eqid ⊢ if 1 ≤ x ⁢ y 1 x ⁢ y ⁢ x 2 = if 1 ≤ x ⁢ y 1 x ⁢ y ⁢ x 2
26 25 reccn2 ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℝ + → ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 w − x < u → 1 w − 1 x < y
27 ovres ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w = x abs ∘ − w
28 eldifi ⊢ x ∈ ℂ ∖ 0 → x ∈ ℂ
29 eldifi ⊢ w ∈ ℂ ∖ 0 → w ∈ ℂ
30 eqid ⊢ abs ∘ − = abs ∘ −
31 30 cnmetdval ⊢ x ∈ ℂ ∧ w ∈ ℂ → x abs ∘ − w = x − w
32 abssub ⊢ x ∈ ℂ ∧ w ∈ ℂ → x − w = w − x
33 31 32 eqtrd ⊢ x ∈ ℂ ∧ w ∈ ℂ → x abs ∘ − w = w − x
34 28 29 33 syl2an ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → x abs ∘ − w = w − x
35 27 34 eqtrd ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w = w − x
36 35 breq1d ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u ↔ w − x < u
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 = w → 1 z = 1 w
41 ovex ⊢ 1 w ∈ V
42 40 20 41 fvmpt ⊢ w ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w = 1 w
43 39 42 oveqan12d ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w = 1 x abs ∘ − 1 w
44 eldifsn ⊢ x ∈ ℂ ∖ 0 ↔ x ∈ ℂ ∧ x ≠ 0
45 reccl ⊢ x ∈ ℂ ∧ x ≠ 0 → 1 x ∈ ℂ
46 44 45 sylbi ⊢ x ∈ ℂ ∖ 0 → 1 x ∈ ℂ
47 eldifsn ⊢ w ∈ ℂ ∖ 0 ↔ w ∈ ℂ ∧ w ≠ 0
48 reccl ⊢ w ∈ ℂ ∧ w ≠ 0 → 1 w ∈ ℂ
49 47 48 sylbi ⊢ w ∈ ℂ ∖ 0 → 1 w ∈ ℂ
50 30 cnmetdval ⊢ 1 x ∈ ℂ ∧ 1 w ∈ ℂ → 1 x abs ∘ − 1 w = 1 x − 1 w
51 abssub ⊢ 1 x ∈ ℂ ∧ 1 w ∈ ℂ → 1 x − 1 w = 1 w − 1 x
52 50 51 eqtrd ⊢ 1 x ∈ ℂ ∧ 1 w ∈ ℂ → 1 x abs ∘ − 1 w = 1 w − 1 x
53 46 49 52 syl2an ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → 1 x abs ∘ − 1 w = 1 w − 1 x
54 43 53 eqtrd ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w = 1 w − 1 x
55 54 breq1d ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y ↔ 1 w − 1 x < y
56 36 55 imbi12d ⊢ x ∈ ℂ ∖ 0 ∧ w ∈ ℂ ∖ 0 → x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y ↔ w − x < u → 1 w − 1 x < y
57 56 ralbidva ⊢ x ∈ ℂ ∖ 0 → ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y ↔ ∀ w ∈ ℂ ∖ 0 w − x < u → 1 w − 1 x < y
58 57 rexbidv ⊢ x ∈ ℂ ∖ 0 → ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y ↔ ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 w − x < u → 1 w − 1 x < y
59 58 adantr ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℝ + → ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y ↔ ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 w − x < u → 1 w − 1 x < y
60 26 59 mpbird ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℝ + → ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y
61 60 rgen2 ⊢ ∀ x ∈ ℂ ∖ 0 ∀ y ∈ ℝ + ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ 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 ⟼ 1 z ∈ K Cn J ↔ z ∈ ℂ ∖ 0 ⟼ 1 z : ℂ ∖ 0 ⟶ ℂ ∧ ∀ x ∈ ℂ ∖ 0 ∀ y ∈ ℝ + ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y
72 64 62 71 mp2an ⊢ z ∈ ℂ ∖ 0 ⟼ 1 z ∈ K Cn J ↔ z ∈ ℂ ∖ 0 ⟼ 1 z : ℂ ∖ 0 ⟶ ℂ ∧ ∀ x ∈ ℂ ∖ 0 ∀ y ∈ ℝ + ∃ u ∈ ℝ + ∀ w ∈ ℂ ∖ 0 x abs ∘ − ↾ ℂ ∖ 0 × ℂ ∖ 0 w < u → z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ x abs ∘ − z ∈ ℂ ∖ 0 ⟼ 1 z ⁡ w < y
73 24 61 72 mpbir2an ⊢ z ∈ ℂ ∖ 0 ⟼ 1 z ∈ K Cn J
74 73 a1i ⊢ ⊤ → z ∈ ℂ ∖ 0 ⟼ 1 z ∈ K Cn J
75 oveq2 ⊢ z = y → 1 z = 1 y
76 13 17 19 17 74 75 cnmpt21 ⊢ ⊤ → x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ 1 y ∈ J × t K Cn J
77 1 mulcn ⊢ × ∈ J × t J Cn J
78 77 a1i ⊢ ⊤ → × ∈ J × t J Cn J
79 13 17 18 76 78 cnmpt22f ⊢ ⊤ → x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ x ⁢ 1 y ∈ J × t K Cn J
80 79 mptru ⊢ x ∈ ℂ , y ∈ ℂ ∖ 0 ⟼ x ⁢ 1 y ∈ J × t K Cn J
81 11 80 eqeltri ⊢ ÷ ∈ J × t K Cn J