Step | Hyp | Ref
| Expression |
1 | | df-div 11633 |
. . 3
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) |
2 | | eldifsn 4720 |
. . . . 5
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) |
3 | | divval 11635 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥)) |
4 | | divrec 11649 |
. . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (𝑥 / 𝑦) = (𝑥 · (1 / 𝑦))) |
5 | 3, 4 | eqtr3d 2780 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
6 | 5 | 3expb 1119 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0)) →
(℩𝑧 ∈
ℂ (𝑦 · 𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
7 | 2, 6 | sylan2b 594 |
. . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥) = (𝑥 · (1 / 𝑦))) |
8 | 7 | mpoeq3ia 7353 |
. . 3
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (℩𝑧
∈ ℂ (𝑦 ·
𝑧) = 𝑥)) = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (𝑥 · (1 / 𝑦))) |
9 | 1, 8 | eqtri 2766 |
. 2
⊢ / =
(𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) |
10 | | addcn.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
11 | 10 | cnfldtopon 23946 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ 𝐽 ∈
(TopOn‘ℂ)) |
13 | | divcn.k |
. . . . 5
⊢ 𝐾 = (𝐽 ↾t (ℂ ∖
{0})) |
14 | | difss 4066 |
. . . . . 6
⊢ (ℂ
∖ {0}) ⊆ ℂ |
15 | | resttopon 22312 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ (ℂ ∖ {0}) ⊆ ℂ) → (𝐽 ↾t (ℂ ∖ {0}))
∈ (TopOn‘(ℂ ∖ {0}))) |
16 | 12, 14, 15 | sylancl 586 |
. . . . 5
⊢ (⊤
→ (𝐽
↾t (ℂ ∖ {0})) ∈ (TopOn‘(ℂ ∖
{0}))) |
17 | 13, 16 | eqeltrid 2843 |
. . . 4
⊢ (⊤
→ 𝐾 ∈
(TopOn‘(ℂ ∖ {0}))) |
18 | 12, 17 | cnmpt1st 22819 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑥) ∈
((𝐽 ×t
𝐾) Cn 𝐽)) |
19 | 12, 17 | cnmpt2nd 22820 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ 𝑦) ∈
((𝐽 ×t
𝐾) Cn 𝐾)) |
20 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) = (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) |
21 | | eldifsn 4720 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℂ ∖ {0})
↔ (𝑧 ∈ ℂ
∧ 𝑧 ≠
0)) |
22 | | reccl 11640 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝑧 ≠ 0) → (1 / 𝑧) ∈
ℂ) |
23 | 21, 22 | sylbi 216 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℂ ∖ {0})
→ (1 / 𝑧) ∈
ℂ) |
24 | 20, 23 | fmpti 6986 |
. . . . . . 7
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)):(ℂ
∖ {0})⟶ℂ |
25 | | eqid 2738 |
. . . . . . . . . 10
⊢ (if(1
≤ ((abs‘𝑥)
· 𝑦), 1,
((abs‘𝑥) ·
𝑦)) ·
((abs‘𝑥) / 2)) =
(if(1 ≤ ((abs‘𝑥)
· 𝑦), 1,
((abs‘𝑥) ·
𝑦)) ·
((abs‘𝑥) /
2)) |
26 | 25 | reccn2 15306 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈
ℝ+) → ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((abs‘(𝑤 −
𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)) |
27 | | ovres 7438 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑤) = (𝑥(abs ∘ − )𝑤)) |
28 | | eldifi 4061 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ∈
ℂ) |
29 | | eldifi 4061 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ 𝑤 ∈
ℂ) |
30 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
31 | 30 | cnmetdval 23934 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥(abs ∘ − )𝑤) = (abs‘(𝑥 − 𝑤))) |
32 | | abssub 15038 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(abs‘(𝑥 − 𝑤)) = (abs‘(𝑤 − 𝑥))) |
33 | 31, 32 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑥(abs ∘ − )𝑤) = (abs‘(𝑤 − 𝑥))) |
34 | 28, 29, 33 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (𝑥(abs
∘ − )𝑤) =
(abs‘(𝑤 − 𝑥))) |
35 | 27, 34 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑤) = (abs‘(𝑤 − 𝑥))) |
36 | 35 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 ↔ (abs‘(𝑤 − 𝑥)) < 𝑢)) |
37 | | oveq2 7283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → (1 / 𝑧) = (1 / 𝑥)) |
38 | | ovex 7308 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑥) ∈
V |
39 | 37, 20, 38 | fvmpt 6875 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑥) = (1 / 𝑥)) |
40 | | oveq2 7283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → (1 / 𝑧) = (1 / 𝑤)) |
41 | | ovex 7308 |
. . . . . . . . . . . . . . . . 17
⊢ (1 /
𝑤) ∈
V |
42 | 40, 20, 41 | fvmpt 6875 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ ((𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧))‘𝑤) = (1 / 𝑤)) |
43 | 39, 42 | oveqan12d 7294 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑤)) = ((1 / 𝑥)(abs ∘ − )(1 / 𝑤))) |
44 | | eldifsn 4720 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
45 | | reccl 11640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (1 / 𝑥) ∈
ℂ) |
46 | 44, 45 | sylbi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (1 / 𝑥) ∈
ℂ) |
47 | | eldifsn 4720 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ (ℂ ∖ {0})
↔ (𝑤 ∈ ℂ
∧ 𝑤 ≠
0)) |
48 | | reccl 11640 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℂ ∧ 𝑤 ≠ 0) → (1 / 𝑤) ∈
ℂ) |
49 | 47, 48 | sylbi 216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (ℂ ∖ {0})
→ (1 / 𝑤) ∈
ℂ) |
50 | 30 | cnmetdval 23934 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑤)) =
(abs‘((1 / 𝑥) −
(1 / 𝑤)))) |
51 | | abssub 15038 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
(abs‘((1 / 𝑥) −
(1 / 𝑤))) = (abs‘((1
/ 𝑤) − (1 / 𝑥)))) |
52 | 50, 51 | eqtrd 2778 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑥) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
((1 / 𝑥)(abs ∘
− )(1 / 𝑤)) =
(abs‘((1 / 𝑤) −
(1 / 𝑥)))) |
53 | 46, 49, 52 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((1 / 𝑥)(abs ∘ − )(1 / 𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑥)))) |
54 | 43, 53 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑥)))) |
55 | 54 | breq1d 5084 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → ((((𝑧
∈ (ℂ ∖ {0}) ↦ (1 / 𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑤)) < 𝑦 ↔ (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦)) |
56 | 36, 55 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑤 ∈ (ℂ
∖ {0})) → (((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ((abs‘(𝑤 − 𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))) |
57 | 56 | ralbidva 3111 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (∀𝑤 ∈
(ℂ ∖ {0})((𝑥((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∀𝑤 ∈ (ℂ ∖
{0})((abs‘(𝑤 −
𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))) |
58 | 57 | rexbidv 3226 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (∃𝑢 ∈
ℝ+ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((abs‘(𝑤 −
𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))) |
59 | 58 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈
ℝ+) → (∃𝑢 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑥((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦) ↔ ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((abs‘(𝑤 −
𝑥)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑥))) < 𝑦))) |
60 | 26, 59 | mpbird 256 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℂ ∖ {0})
∧ 𝑦 ∈
ℝ+) → ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ (ℂ ∖
{0})((𝑥((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦)) |
61 | 60 | rgen2 3120 |
. . . . . . 7
⊢
∀𝑥 ∈
(ℂ ∖ {0})∀𝑦 ∈ ℝ+ ∃𝑢 ∈ ℝ+
∀𝑤 ∈ (ℂ
∖ {0})((𝑥((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦) |
62 | | cnxmet 23936 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
63 | | xmetres2 23514 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → ((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0}))) ∈ (∞Met‘(ℂ ∖
{0}))) |
64 | 62, 14, 63 | mp2an 689 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) ∈ (∞Met‘(ℂ ∖ {0})) |
65 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))) = ((abs ∘ − ) ↾ ((ℂ ∖ {0}) ×
(ℂ ∖ {0}))) |
66 | 10 | cnfldtopn 23945 |
. . . . . . . . . . . 12
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
67 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ ((ℂ ∖ {0})
× (ℂ ∖ {0})))) = (MetOpen‘((abs ∘ − )
↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
68 | 65, 66, 67 | metrest 23680 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (ℂ ∖ {0})
⊆ ℂ) → (𝐽
↾t (ℂ ∖ {0})) = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0}))))) |
69 | 62, 14, 68 | mp2an 689 |
. . . . . . . . . 10
⊢ (𝐽 ↾t (ℂ
∖ {0})) = (MetOpen‘((abs ∘ − ) ↾ ((ℂ
∖ {0}) × (ℂ ∖ {0})))) |
70 | 13, 69 | eqtri 2766 |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ((ℂ ∖ {0}) × (ℂ ∖
{0})))) |
71 | 70, 66 | metcn 23699 |
. . . . . . . 8
⊢ ((((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 689 |
. . . . . . 7
⊢ ((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) ↔ ((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧)):(ℂ ∖
{0})⟶ℂ ∧ ∀𝑥 ∈ (ℂ ∖ {0})∀𝑦 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ (ℂ ∖ {0})((𝑥((abs ∘ − ) ↾
((ℂ ∖ {0}) × (ℂ ∖ {0})))𝑤) < 𝑢 → (((𝑧 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑧))‘𝑥)(abs ∘ − )((𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧))‘𝑤)) < 𝑦))) |
73 | 24, 61, 72 | mpbir2an 708 |
. . . . . 6
⊢ (𝑧 ∈ (ℂ ∖ {0})
↦ (1 / 𝑧)) ∈
(𝐾 Cn 𝐽) |
74 | 73 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑧 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑧)) ∈ (𝐾 Cn 𝐽)) |
75 | | oveq2 7283 |
. . . . 5
⊢ (𝑧 = 𝑦 → (1 / 𝑧) = (1 / 𝑦)) |
76 | 12, 17, 19, 17, 74, 75 | cnmpt21 22822 |
. . . 4
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (1 / 𝑦))
∈ ((𝐽
×t 𝐾) Cn
𝐽)) |
77 | 10 | mulcn 24030 |
. . . . 5
⊢ ·
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
78 | 77 | a1i 11 |
. . . 4
⊢ (⊤
→ · ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
79 | 12, 17, 18, 76, 78 | cnmpt22f 22826 |
. . 3
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ (ℂ ∖
{0}) ↦ (𝑥 · (1
/ 𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
80 | 79 | mptru 1546 |
. 2
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0})
↦ (𝑥 · (1 /
𝑦))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽) |
81 | 9, 80 | eqeltri 2835 |
1
⊢ / ∈
((𝐽 ×t
𝐾) Cn 𝐽) |