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

Proof

Step Hyp Ref Expression
1 addcn.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 eldifsn ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) )
22 reccl ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑧 ≠ 0 ) → ( 1 / 𝑧 ) ∈ ℂ )
23 21 22 sylbi ⊢ ( 𝑧 ∈ ( ℂ ∖ { 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 eldifsn ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
45 reccl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
46 44 45 sylbi ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑥 ) ∈ ℂ )
47 eldifsn ⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) )
48 reccl ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑤 ≠ 0 ) → ( 1 / 𝑤 ) ∈ ℂ )
49 47 48 sylbi ⊢ ( 𝑤 ∈ ( ℂ ∖ { 0 } ) → ( 1 / 𝑤 ) ∈ ℂ )
50 30 cnmetdval ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑤 ) ) ) )
51 abssub ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( abs ‘ ( ( 1 / 𝑥 ) − ( 1 / 𝑤 ) ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
52 50 51 eqtrd ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ ( 1 / 𝑤 ) ∈ ℂ ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
53 46 49 52 syl2an ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / 𝑥 ) ( abs ∘ − ) ( 1 / 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
54 43 53 eqtrd ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) = ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) )
55 54 breq1d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ↔ ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) )
56 36 55 imbi12d ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑤 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
57 56 ralbidva ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
58 57 rexbidv ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
59 58 adantr ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑢 → ( abs ‘ ( ( 1 / 𝑤 ) − ( 1 / 𝑥 ) ) ) < 𝑦 ) ) )
60 26 59 mpbird ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) )
61 60 rgen2 ⊢ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 )
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 ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
67 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
68 65 66 67 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ) )
69 62 14 68 mp2an ⊢ ( 𝐽 ↾t ( ℂ ∖ { 0 } ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
70 2 69 eqtri ⊢ 𝐾 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) )
71 70 66 metcn ⊢ ( ( ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) ∈ ( ∞Met ‘ ( ℂ ∖ { 0 } ) ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) → ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ) ) )
72 64 62 71 mp2an ⊢ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) ↔ ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) : ( ℂ ∖ { 0 } ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ℝ+ ∃ 𝑢 ∈ ℝ+ ∀ 𝑤 ∈ ( ℂ ∖ { 0 } ) ( ( 𝑥 ( ( abs ∘ − ) ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑤 ) < 𝑢 → ( ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑥 ) ( abs ∘ − ) ( ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ‘ 𝑤 ) ) < 𝑦 ) ) )
73 24 61 72 mpbir2an ⊢ ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 )
74 73 a1i ⊢ ( ⊤ → ( 𝑧 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑧 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
75 oveq2 ⊢ ( 𝑧 = 𝑦 → ( 1 / 𝑧 ) = ( 1 / 𝑦 ) )
76 13 17 19 17 74 75 cnmpt21 ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
77 1 mulcn ⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
78 77 a1i ⊢ ( ⊤ → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
79 13 17 18 76 78 cnmpt22f ⊢ ( ⊤ → ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 ) )
80 79 mptru ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( 1 / 𝑦 ) ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 )
81 11 80 eqeltri ⊢ / ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐽 )