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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
divcn.k ⊢ 𝐾 = ( 𝐽 ↾t ( ℂ ∖ { 0 } ) )
Assertion divcn / ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 )

Proof

Step Hyp Ref Expression
1 mpomulcn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 divcn.k ⊢ 𝐾 = ( 𝐽 ↾t ( ℂ ∖ { 0 } ) )
3 df-div ⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
4 eldifsn ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
5 divval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
6 divrec ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
7 5 6 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
8 7 3expb ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
9 4 8 sylan2b ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
10 9 mpoeq3ia ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) )
11 3 10 eqtri ⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) )
12 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
13 12 a1i ⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
14 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
15 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
16 13 14 15 sylancl ⊢ ( ⊤ → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
17 2 16 eqeltrid ⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
18 13 17 cnmpt1st ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
19 13 17 cnmpt2nd ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
20 eqid ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) = ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) )
21 eldifi ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ∈ ℂ )
22 eldifsni ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → 𝑧 ≠ 0 )
23 21 22 reccld ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑧 ) ∈ ℂ )
24 20 23 fmpti ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ
25 eqid ⊢ ( if ( 1 ≤ ( ( abs ‘ 𝑥 ) · 𝑤 ) , 1 , ( ( abs ‘ 𝑥 ) · 𝑤 ) ) · ( ( abs ‘ 𝑥 ) / 2 ) ) = ( if ( 1 ≤ ( ( abs ‘ 𝑥 ) · 𝑤 ) , 1 , ( ( abs ‘ 𝑥 ) · 𝑤 ) ) · ( ( abs ‘ 𝑥 ) / 2 ) )
26 25 reccn2 ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 → ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) )
27 ovres ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) = ( 𝑥 ( abs ∘ − ) 𝑦 ) )
28 eldifi ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
29 eldifi ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
30 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
31 30 cnmetdval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑥 − 𝑦 ) ) )
32 abssub ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
33 31 32 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
34 28 29 33 syl2an ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
35 27 34 eqtrd ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) = ( abs ‘ ( 𝑦 − 𝑥 ) ) )
36 35 breq1d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 ↔ ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 ) )
37 oveq2 ⊢ ( 𝑧 = 𝑥 → ( 1 / 𝑧 ) = ( 1 / 𝑥 ) )
38 ovex ⊢ ( 1 / 𝑥 ) ∈ V
39 37 20 38 fvmpt ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) = ( 1 / 𝑥 ) )
40 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 1 / 𝑧 ) = ( 1 / 𝑦 ) )
41 ovex ⊢ ( 1 / 𝑦 ) ∈ V
42 40 20 41 fvmpt ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) = ( 1 / 𝑦 ) )
43 39 42 oveqan12d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) = ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑦 ) ) )
44 eldifsni ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
45 28 44 reccld ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ ℂ )
46 eldifsni ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
47 29 46 reccld ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑦 ) ∈ ℂ )
48 30 cnmetdval ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑦 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑦 ) ) = ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑦 ) ) ) )
49 abssub ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑦 ) ∈ ℂ ) → ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑦 ) ) ) = ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) )
50 48 49 eqtrd ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑦 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑦 ) ) = ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) )
51 45 47 50 syl2an ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑦 ) ) = ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) )
52 43 51 eqtrd ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) = ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) )
53 52 breq1d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ↔ ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) )
54 36 53 imbi12d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 → ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) ) )
55 54 ralbidva ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ↔ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 → ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) ) )
56 55 rexbidv ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ↔ ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 → ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) ) )
57 56 adantr ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ↔ ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑦 − 𝑥 ) ) < 𝑎 → ( abs ‘ ( ( 1 / 𝑦 ) − ( 1 / 𝑥 ) ) ) < 𝑤 ) ) )
58 26 57 mpbird ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) )
59 58 rgen2 ⊢ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑤 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 )
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 ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
65 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
66 63 64 65 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) )
67 60 14 66 mp2an ⊢ ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
68 2 67 eqtri ⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
69 68 64 metcn ⊢ ( ( ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ∈ ( ∞Met ‘ ( ℂ ∖ { 0 } ) ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑤 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ) ) )
70 62 60 69 mp2an ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑤 ∈ ℝ+ ∃ 𝑎 ∈ ℝ+ ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) < 𝑎 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑦 ) ) < 𝑤 ) ) )
71 24 59 70 mpbir2an ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 )
72 71 a1i ⊢ ( ⊤ → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
73 13 17 19 17 72 40 cnmpt21 ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
74 1 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
75 74 a1i ⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
76 oveq12 ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 1 / 𝑦 ) ) → ( 𝑢 · 𝑣 ) = ( 𝑥 · ( 1 / 𝑦 ) ) )
77 13 17 18 73 13 13 75 76 cnmpt22 ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
78 77 mptru ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 )
79 11 78 eqeltri ⊢ / ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 )