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 𝐽 )