Step | Hyp | Ref
| Expression |
1 | | mulcl 9899 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
2 | | mulc1cncf.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) |
3 | 1, 2 | fmptd 6292 |
. 2
⊢ (𝐴 ∈ ℂ → 𝐹:ℂ⟶ℂ) |
4 | | simprr 792 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑧 ∈
ℝ+) |
5 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝐴 ∈
ℂ) |
6 | | simprl 790 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑦 ∈
ℂ) |
7 | | mulcn2 14174 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
∧ 𝐴 ∈ ℂ
∧ 𝑦 ∈ ℂ)
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
8 | 4, 5, 6, 7 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
9 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝐴 → (𝑣 − 𝐴) = (𝐴 − 𝐴)) |
10 | 9 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (abs‘(𝑣 − 𝐴)) = (abs‘(𝐴 − 𝐴))) |
11 | 10 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → ((abs‘(𝑣 − 𝐴)) < 𝑡 ↔ (abs‘(𝐴 − 𝐴)) < 𝑡)) |
12 | 11 | anbi1d 737 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
13 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝐴 → (𝑣 · 𝑢) = (𝐴 · 𝑢)) |
14 | 13 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → ((𝑣 · 𝑢) − (𝐴 · 𝑦)) = ((𝐴 · 𝑢) − (𝐴 · 𝑦))) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
16 | 15 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ((abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
17 | 12, 16 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ((((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
18 | 17 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐴 → (∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
19 | 18 | rspcv 3278 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
20 | 19 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
21 | | subid 10179 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) |
22 | 21 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 − 𝐴) = 0) |
23 | 22 | abs00bd 13879 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) = 0) |
24 | | simprll 798 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑡 ∈ ℝ+) |
25 | 24 | rpgt0d 11751 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 0 < 𝑡) |
26 | 23, 25 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) < 𝑡) |
27 | 26 | biantrurd 528 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘(𝑢 − 𝑦)) < 𝑤 ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
28 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑢 ∈ ℂ) |
29 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) |
30 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑢) ∈ V |
31 | 29, 2, 30 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
32 | 28, 31 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
33 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑦 ∈ ℂ) |
34 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
35 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑦) ∈ V |
36 | 34, 2, 35 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
37 | 33, 36 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
38 | 32, 37 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((𝐹‘𝑢) − (𝐹‘𝑦)) = ((𝐴 · 𝑢) − (𝐴 · 𝑦))) |
39 | 38 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
40 | 39 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
41 | 27, 40 | imbi12d 333 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
42 | 41 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) ∧ 𝑢 ∈ ℂ) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
43 | 42 | ralbidva 2968 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
44 | 20, 43 | sylibrd 248 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
45 | 44 | anassrs 678 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) ∧ 𝑤 ∈ ℝ+) →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
46 | 45 | reximdva 3000 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
47 | 46 | rexlimdva 3013 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ (∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
48 | 8, 47 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
49 | 48 | ralrimivva 2954 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈ ℂ
∀𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
50 | | ssid 3587 |
. . 3
⊢ ℂ
⊆ ℂ |
51 | | elcncf2 22501 |
. . 3
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)))) |
52 | 50, 50, 51 | mp2an 704 |
. 2
⊢ (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
53 | 3, 49, 52 | sylanbrc 695 |
1
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |