Step | Hyp | Ref
| Expression |
1 | | breq1 3990 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝑥 # 0 ↔ 𝑧 # 0)) |
2 | 1 | elrab 2886 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑧 ∈ ℂ ∧ 𝑧 # 0)) |
3 | | divrecap 8592 |
. . . . 5
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ∧ 𝑧 # 0) → (𝑦 / 𝑧) = (𝑦 · (1 / 𝑧))) |
4 | 3 | 3expb 1199 |
. . . 4
⊢ ((𝑦 ∈ ℂ ∧ (𝑧 ∈ ℂ ∧ 𝑧 # 0)) → (𝑦 / 𝑧) = (𝑦 · (1 / 𝑧))) |
5 | 2, 4 | sylan2b 285 |
. . 3
⊢ ((𝑦 ∈ ℂ ∧ 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑦 / 𝑧) = (𝑦 · (1 / 𝑧))) |
6 | 5 | mpoeq3ia 5915 |
. 2
⊢ (𝑦 ∈ ℂ, 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 / 𝑧)) = (𝑦 ∈ ℂ, 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 · (1 / 𝑧))) |
7 | | addcncntop.j |
. . . . . 6
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
8 | 7 | cntoptopon 13285 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℂ) |
9 | 8 | a1i 9 |
. . . 4
⊢ (⊤
→ 𝐽 ∈
(TopOn‘ℂ)) |
10 | | divcnap.k |
. . . . 5
⊢ 𝐾 = (𝐽 ↾t {𝑥 ∈ ℂ ∣ 𝑥 # 0}) |
11 | | ssrab2 3232 |
. . . . . 6
⊢ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ⊆
ℂ |
12 | | resttopon 12924 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘ℂ)
∧ {𝑥 ∈ ℂ
∣ 𝑥 # 0} ⊆
ℂ) → (𝐽
↾t {𝑥
∈ ℂ ∣ 𝑥 #
0}) ∈ (TopOn‘{𝑥
∈ ℂ ∣ 𝑥 #
0})) |
13 | 9, 11, 12 | sylancl 411 |
. . . . 5
⊢ (⊤
→ (𝐽
↾t {𝑥
∈ ℂ ∣ 𝑥 #
0}) ∈ (TopOn‘{𝑥
∈ ℂ ∣ 𝑥 #
0})) |
14 | 10, 13 | eqeltrid 2257 |
. . . 4
⊢ (⊤
→ 𝐾 ∈
(TopOn‘{𝑥 ∈
ℂ ∣ 𝑥 #
0})) |
15 | 9, 14 | cnmpt1st 13041 |
. . . 4
⊢ (⊤
→ (𝑦 ∈ ℂ,
𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
16 | 9, 14 | cnmpt2nd 13042 |
. . . . 5
⊢ (⊤
→ (𝑦 ∈ ℂ,
𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ 𝑧) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
17 | | eqid 2170 |
. . . . . . . 8
⊢ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) = (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) |
18 | | breq1 3990 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑞 → (𝑥 # 0 ↔ 𝑞 # 0)) |
19 | 18 | elrab 2886 |
. . . . . . . . 9
⊢ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑞 ∈ ℂ ∧ 𝑞 # 0)) |
20 | | recclap 8583 |
. . . . . . . . 9
⊢ ((𝑞 ∈ ℂ ∧ 𝑞 # 0) → (1 / 𝑞) ∈
ℂ) |
21 | 19, 20 | sylbi 120 |
. . . . . . . 8
⊢ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (1 / 𝑞) ∈ ℂ) |
22 | 17, 21 | fmpti 5645 |
. . . . . . 7
⊢ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)):{𝑥 ∈ ℂ ∣ 𝑥 # 0}⟶ℂ |
23 | | breq1 3990 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (𝑥 # 0 ↔ 𝑎 # 0)) |
24 | 23 | elrab 2886 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑎 ∈ ℂ ∧ 𝑎 # 0)) |
25 | | eqid 2170 |
. . . . . . . . . . . 12
⊢ (inf({1,
((abs‘𝑎) ·
𝑏)}, ℝ, < )
· ((abs‘𝑎) /
2)) = (inf({1, ((abs‘𝑎) · 𝑏)}, ℝ, < ) ·
((abs‘𝑎) /
2)) |
26 | 25 | reccn2ap 11263 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ℂ ∧ 𝑎 # 0 ∧ 𝑏 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏)) |
27 | 26 | 3expa 1198 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℂ ∧ 𝑎 # 0) ∧ 𝑏 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏)) |
28 | 24, 27 | sylanb 282 |
. . . . . . . . 9
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑏 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏)) |
29 | | ovres 5989 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) = (𝑎(abs ∘ − )𝑤)) |
30 | | elrabi 2883 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → 𝑎 ∈ ℂ) |
31 | | elrabi 2883 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → 𝑤 ∈ ℂ) |
32 | | eqid 2170 |
. . . . . . . . . . . . . . . . . 18
⊢ (abs
∘ − ) = (abs ∘ − ) |
33 | 32 | cnmetdval 13282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑎(abs ∘ − )𝑤) = (abs‘(𝑎 − 𝑤))) |
34 | | abssub 11052 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ ℂ ∧ 𝑤 ∈ ℂ) →
(abs‘(𝑎 − 𝑤)) = (abs‘(𝑤 − 𝑎))) |
35 | 33, 34 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (𝑎(abs ∘ − )𝑤) = (abs‘(𝑤 − 𝑎))) |
36 | 30, 31, 35 | syl2an 287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑎(abs ∘ − )𝑤) = (abs‘(𝑤 − 𝑎))) |
37 | 29, 36 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) = (abs‘(𝑤 − 𝑎))) |
38 | 37 | breq1d 3997 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 ↔ (abs‘(𝑤 − 𝑎)) < 𝑢)) |
39 | 24 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → 𝑎 # 0) |
40 | 30, 39 | recclapd 8685 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (1 / 𝑎) ∈ ℂ) |
41 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 𝑎 → (1 / 𝑞) = (1 / 𝑎)) |
42 | 41, 17 | fvmptg 5570 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ (1 / 𝑎) ∈ ℂ) → ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎) = (1 / 𝑎)) |
43 | 40, 42 | mpdan 419 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎) = (1 / 𝑎)) |
44 | | breq1 3990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑥 # 0 ↔ 𝑤 # 0)) |
45 | 44 | elrab 2886 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↔ (𝑤 ∈ ℂ ∧ 𝑤 # 0)) |
46 | 45 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → 𝑤 # 0) |
47 | 31, 46 | recclapd 8685 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (1 / 𝑤) ∈ ℂ) |
48 | | oveq2 5858 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 = 𝑤 → (1 / 𝑞) = (1 / 𝑤)) |
49 | 48, 17 | fvmptg 5570 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ (1 / 𝑤) ∈ ℂ) → ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤) = (1 / 𝑤)) |
50 | 47, 49 | mpdan 419 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤) = (1 / 𝑤)) |
51 | 43, 50 | oveqan12d 5869 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) = ((1 / 𝑎)(abs ∘ − )(1 / 𝑤))) |
52 | 32 | cnmetdval 13282 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑎) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
((1 / 𝑎)(abs ∘
− )(1 / 𝑤)) =
(abs‘((1 / 𝑎) −
(1 / 𝑤)))) |
53 | | abssub 11052 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 /
𝑎) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
(abs‘((1 / 𝑎) −
(1 / 𝑤))) = (abs‘((1
/ 𝑤) − (1 / 𝑎)))) |
54 | 52, 53 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
⊢ (((1 /
𝑎) ∈ ℂ ∧ (1
/ 𝑤) ∈ ℂ) →
((1 / 𝑎)(abs ∘
− )(1 / 𝑤)) =
(abs‘((1 / 𝑤) −
(1 / 𝑎)))) |
55 | 40, 47, 54 | syl2an 287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → ((1 / 𝑎)(abs ∘ − )(1 / 𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑎)))) |
56 | 51, 55 | eqtrd 2203 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) = (abs‘((1 / 𝑤) − (1 / 𝑎)))) |
57 | 56 | breq1d 3997 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → ((((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏 ↔ (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏)) |
58 | 38, 57 | imbi12d 233 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}) → (((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏) ↔ ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏))) |
59 | 58 | ralbidva 2466 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏) ↔ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏))) |
60 | 59 | rexbidv 2471 |
. . . . . . . . . 10
⊢ (𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} → (∃𝑢 ∈ ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏) ↔ ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏))) |
61 | 60 | adantr 274 |
. . . . . . . . 9
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑏 ∈ ℝ+) →
(∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏) ↔ ∃𝑢 ∈ ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((abs‘(𝑤 − 𝑎)) < 𝑢 → (abs‘((1 / 𝑤) − (1 / 𝑎))) < 𝑏))) |
62 | 28, 61 | mpbird 166 |
. . . . . . . 8
⊢ ((𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ∧ 𝑏 ∈ ℝ+) →
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏)) |
63 | 62 | rgen2 2556 |
. . . . . . 7
⊢
∀𝑎 ∈
{𝑥 ∈ ℂ ∣
𝑥 # 0}∀𝑏 ∈ ℝ+
∃𝑢 ∈
ℝ+ ∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏) |
64 | | cnxmet 13284 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
65 | | xmetres2 13132 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ⊆ ℂ) → ((abs ∘
− ) ↾ ({𝑥
∈ ℂ ∣ 𝑥 #
0} × {𝑥 ∈
ℂ ∣ 𝑥 # 0}))
∈ (∞Met‘{𝑥
∈ ℂ ∣ 𝑥 #
0})) |
66 | 64, 11, 65 | mp2an 424 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0})) ∈ (∞Met‘{𝑥 ∈ ℂ ∣ 𝑥 # 0}) |
67 | | eqid 2170 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0})) = ((abs ∘ − ) ↾
({𝑥 ∈ ℂ ∣
𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0})) |
68 | | eqid 2170 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))) = (MetOpen‘((abs ∘
− ) ↾ ({𝑥
∈ ℂ ∣ 𝑥 #
0} × {𝑥 ∈
ℂ ∣ 𝑥 #
0}))) |
69 | 67, 7, 68 | metrest 13259 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ⊆ ℂ) → (𝐽 ↾t {𝑥 ∈ ℂ ∣ 𝑥 # 0}) = (MetOpen‘((abs
∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0})))) |
70 | 64, 11, 69 | mp2an 424 |
. . . . . . . . . 10
⊢ (𝐽 ↾t {𝑥 ∈ ℂ ∣ 𝑥 # 0}) = (MetOpen‘((abs
∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))) |
71 | 10, 70 | eqtri 2191 |
. . . . . . . . 9
⊢ 𝐾 = (MetOpen‘((abs ∘
− ) ↾ ({𝑥
∈ ℂ ∣ 𝑥 #
0} × {𝑥 ∈
ℂ ∣ 𝑥 #
0}))) |
72 | 71, 7 | metcn 13267 |
. . . . . . . 8
⊢ ((((abs
∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0})) ∈ (∞Met‘{𝑥 ∈ ℂ ∣ 𝑥 # 0}) ∧ (abs ∘
− ) ∈ (∞Met‘ℂ)) → ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) ∈ (𝐾 Cn 𝐽) ↔ ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)):{𝑥 ∈ ℂ ∣ 𝑥 # 0}⟶ℂ ∧ ∀𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}∀𝑏 ∈ ℝ+ ∃𝑢 ∈ ℝ+
∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏)))) |
73 | 66, 64, 72 | mp2an 424 |
. . . . . . 7
⊢ ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) ∈ (𝐾 Cn 𝐽) ↔ ((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)):{𝑥 ∈ ℂ ∣ 𝑥 # 0}⟶ℂ ∧ ∀𝑎 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0}∀𝑏 ∈ ℝ+ ∃𝑢 ∈ ℝ+
∀𝑤 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ((𝑎((abs ∘ − ) ↾ ({𝑥 ∈ ℂ ∣ 𝑥 # 0} × {𝑥 ∈ ℂ ∣ 𝑥 # 0}))𝑤) < 𝑢 → (((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑎)(abs ∘ − )((𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞))‘𝑤)) < 𝑏))) |
74 | 22, 63, 73 | mpbir2an 937 |
. . . . . 6
⊢ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) ∈ (𝐾 Cn 𝐽) |
75 | 74 | a1i 9 |
. . . . 5
⊢ (⊤
→ (𝑞 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑞)) ∈ (𝐾 Cn 𝐽)) |
76 | | oveq2 5858 |
. . . . 5
⊢ (𝑞 = 𝑧 → (1 / 𝑞) = (1 / 𝑧)) |
77 | 9, 14, 16, 14, 75, 76 | cnmpt21 13044 |
. . . 4
⊢ (⊤
→ (𝑦 ∈ ℂ,
𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (1 / 𝑧)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
78 | 7 | mulcncntop 13307 |
. . . . 5
⊢ ·
∈ ((𝐽
×t 𝐽) Cn
𝐽) |
79 | 78 | a1i 9 |
. . . 4
⊢ (⊤
→ · ∈ ((𝐽
×t 𝐽) Cn
𝐽)) |
80 | 9, 14, 15, 77, 79 | cnmpt22f 13048 |
. . 3
⊢ (⊤
→ (𝑦 ∈ ℂ,
𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 · (1 / 𝑧))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
81 | 80 | mptru 1357 |
. 2
⊢ (𝑦 ∈ ℂ, 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 · (1 / 𝑧))) ∈ ((𝐽 ×t 𝐾) Cn 𝐽) |
82 | 6, 81 | eqeltri 2243 |
1
⊢ (𝑦 ∈ ℂ, 𝑧 ∈ {𝑥 ∈ ℂ ∣ 𝑥 # 0} ↦ (𝑦 / 𝑧)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽) |