Step | Hyp | Ref
| Expression |
1 | | mpomulcn.j |
. 2
⊢ 𝐽 =
(TopOpen‘ℂfld) |
2 | | mpomulf 11200 |
. 2
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)):(ℂ ×
ℂ)⟶ℂ |
3 | | mulcn2 15537 |
. . 3
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ ∃𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑑 ∈ ℂ ∀𝑒 ∈ ℂ
(((abs‘(𝑑 −
𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎)) |
4 | | simplr 766 |
. . . . . . . . . . . 12
⊢ (((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ))
→ 𝑢 ∈
ℂ) |
5 | | simplll 772 |
. . . . . . . . . . . . 13
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ))
∧ 𝑑 = 𝑢) → 𝑣 ∈ ℂ) |
6 | | simplr 766 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → 𝑑 = 𝑢) |
7 | 6 | fvoveq1d 7423 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (abs‘(𝑑 − 𝑏)) = (abs‘(𝑢 − 𝑏))) |
8 | 7 | breq1d 5148 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → ((abs‘(𝑑 − 𝑏)) < 𝑧 ↔ (abs‘(𝑢 − 𝑏)) < 𝑧)) |
9 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → 𝑒 = 𝑣) |
10 | 9 | fvoveq1d 7423 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (abs‘(𝑒 − 𝑐)) = (abs‘(𝑣 − 𝑐))) |
11 | 10 | breq1d 5148 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → ((abs‘(𝑒 − 𝑐)) < 𝑤 ↔ (abs‘(𝑣 − 𝑐)) < 𝑤)) |
12 | 8, 11 | anbi12d 630 |
. . . . . . . . . . . . . 14
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (((abs‘(𝑑 − 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) ↔ ((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤))) |
13 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → 𝑑 = 𝑢) |
14 | 13 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → 𝑢 = 𝑑) |
15 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → 𝑒 = 𝑣) |
16 | 15 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → 𝑣 = 𝑒) |
17 | 14, 16 | oveq12d 7419 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → (𝑢 · 𝑣) = (𝑑 · 𝑒)) |
18 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) → 𝑢 ∈ ℂ) |
19 | | simplll 772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → 𝑣 ∈ ℂ) |
20 | | tru 1537 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
⊤ |
21 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = 𝑢 → (𝑥 · 𝑦) = (𝑢 · 𝑦)) |
22 | | oveq2 7409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑣 → (𝑢 · 𝑦) = (𝑢 · 𝑣)) |
23 | 21, 22 | cbvmpov 7496 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⊤
→ (𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 · 𝑦)) = (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))) |
25 | | eqidd 2725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⊤
→ 〈𝑢, 𝑣〉 = 〈𝑢, 𝑣〉) |
26 | | mulcl 11190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 · 𝑣) ∈ ℂ) |
27 | 26 | 3adant1 1127 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((⊤ ∧ 𝑢
∈ ℂ ∧ 𝑣
∈ ℂ) → (𝑢
· 𝑣) ∈
ℂ) |
28 | 24, 25, 27 | fvmpopr2d 7562 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((⊤ ∧ 𝑢
∈ ℂ ∧ 𝑣
∈ ℂ) → ((𝑥
∈ ℂ, 𝑦 ∈
ℂ ↦ (𝑥 ·
𝑦))‘〈𝑢, 𝑣〉) = (𝑢 · 𝑣)) |
29 | 28 | eqcomd 2730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((⊤ ∧ 𝑢
∈ ℂ ∧ 𝑣
∈ ℂ) → (𝑢
· 𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑢, 𝑣〉)) |
30 | 20, 29 | mp3an1 1444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 · 𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑢, 𝑣〉)) |
31 | | df-ov 7404 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑢, 𝑣〉) |
32 | 30, 31 | eqtr4di 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 · 𝑣) = (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣)) |
33 | 18, 19, 32 | syl2an2r 682 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → (𝑢 · 𝑣) = (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣)) |
34 | 17, 33 | eqtr3d 2766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ 𝑑 = 𝑢) ∧ 𝑒 = 𝑣) → (𝑑 · 𝑒) = (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣)) |
35 | 34 | adantllr 716 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (𝑑 · 𝑒) = (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣)) |
36 | | df-ov 7404 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐) = ((𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))‘〈𝑏, 𝑐〉) |
37 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑏 → (𝑥 · 𝑦) = (𝑏 · 𝑦)) |
38 | | oveq2 7409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = 𝑐 → (𝑏 · 𝑦) = (𝑏 · 𝑐)) |
39 | 37, 38 | cbvmpov 7496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (𝑏 ∈ ℂ, 𝑐 ∈ ℂ ↦ (𝑏 · 𝑐)) |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ ℝ+
→ (𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 · 𝑦)) = (𝑏 ∈ ℂ, 𝑐 ∈ ℂ ↦ (𝑏 · 𝑐))) |
41 | | eqidd 2725 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ ℝ+
→ 〈𝑏, 𝑐〉 = 〈𝑏, 𝑐〉) |
42 | | mulcl 11190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → (𝑏 · 𝑐) ∈ ℂ) |
43 | 42 | 3adant1 1127 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (𝑏 · 𝑐) ∈
ℂ) |
44 | 40, 41, 43 | fvmpopr2d 7562 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ ((𝑥 ∈ ℂ,
𝑦 ∈ ℂ ↦
(𝑥 · 𝑦))‘〈𝑏, 𝑐〉) = (𝑏 · 𝑐)) |
45 | 36, 44 | eqtr2id 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (𝑏 · 𝑐) = (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐)) |
46 | 45 | ad3antlr 728 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (𝑏 · 𝑐) = (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐)) |
47 | 35, 46 | oveq12d 7419 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → ((𝑑 · 𝑒) − (𝑏 · 𝑐)) = ((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) |
48 | 47 | fveq2d 6885 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) = (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐)))) |
49 | 48 | breq1d 5148 |
. . . . . . . . . . . . . 14
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → ((abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎 ↔ (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎)) |
50 | 12, 49 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢
(((((𝑣 ∈
ℂ ∧ 𝑢 ∈
ℂ) ∧ (𝑎 ∈
ℝ+ ∧ 𝑏
∈ ℂ ∧ 𝑐
∈ ℂ)) ∧ 𝑑 =
𝑢) ∧ 𝑒 = 𝑣) → ((((abs‘(𝑑 − 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) ↔ (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
51 | 5, 50 | rspcdv 3596 |
. . . . . . . . . . . 12
⊢ ((((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ))
∧ 𝑑 = 𝑢) → (∀𝑒 ∈ ℂ
(((abs‘(𝑑 −
𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
52 | 4, 51 | rspcimdv 3594 |
. . . . . . . . . . 11
⊢ (((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) ∧ (𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ))
→ (∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
53 | 52 | expimpd 453 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
∧ ∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎)) → (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
54 | 53 | ex 412 |
. . . . . . . . 9
⊢ (𝑣 ∈ ℂ → (𝑢 ∈ ℂ → (((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
∧ ∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎)) → (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎)))) |
55 | 54 | com13 88 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
∧ ∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎)) → (𝑢 ∈ ℂ → (𝑣 ∈ ℂ → (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎)))) |
56 | 55 | ralrimdv 3144 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
∧ ∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎)) → (𝑢 ∈ ℂ → ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
57 | 56 | ex 412 |
. . . . . 6
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → (𝑢 ∈ ℂ → ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎)))) |
58 | 57 | ralrimdv 3144 |
. . . . 5
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (∀𝑑 ∈
ℂ ∀𝑒 ∈
ℂ (((abs‘(𝑑
− 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
59 | 58 | reximdv 3162 |
. . . 4
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (∃𝑤 ∈
ℝ+ ∀𝑑 ∈ ℂ ∀𝑒 ∈ ℂ (((abs‘(𝑑 − 𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
60 | 59 | reximdv 3162 |
. . 3
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ (∃𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑑 ∈ ℂ ∀𝑒 ∈ ℂ
(((abs‘(𝑑 −
𝑏)) < 𝑧 ∧ (abs‘(𝑒 − 𝑐)) < 𝑤) → (abs‘((𝑑 · 𝑒) − (𝑏 · 𝑐))) < 𝑎) → ∃𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑢 ∈ ℂ
∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎))) |
61 | 3, 60 | mpd 15 |
. 2
⊢ ((𝑎 ∈ ℝ+
∧ 𝑏 ∈ ℂ
∧ 𝑐 ∈ ℂ)
→ ∃𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝑏)) < 𝑧 ∧ (abs‘(𝑣 − 𝑐)) < 𝑤) → (abs‘((𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) − (𝑏(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑐))) < 𝑎)) |
62 | 1, 2, 61 | addcnlem 24702 |
1
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) |