Step | Hyp | Ref
| Expression |
1 | | mulcl 7838 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
2 | | mulc1cncf.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) |
3 | 1, 2 | fmptd 5614 |
. 2
⊢ (𝐴 ∈ ℂ → 𝐹:ℂ⟶ℂ) |
4 | | simprr 522 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑧 ∈
ℝ+) |
5 | | simpl 108 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝐴 ∈
ℂ) |
6 | | simprl 521 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑦 ∈
ℂ) |
7 | | mulcn2 11186 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
∧ 𝐴 ∈ ℂ
∧ 𝑦 ∈ ℂ)
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
8 | 4, 5, 6, 7 | syl3anc 1217 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
9 | | fvoveq1 5837 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (abs‘(𝑣 − 𝐴)) = (abs‘(𝐴 − 𝐴))) |
10 | 9 | breq1d 3971 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → ((abs‘(𝑣 − 𝐴)) < 𝑡 ↔ (abs‘(𝐴 − 𝐴)) < 𝑡)) |
11 | 10 | anbi1d 461 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
12 | | oveq1 5821 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (𝑣 · 𝑢) = (𝐴 · 𝑢)) |
13 | 12 | fvoveq1d 5836 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
14 | 13 | breq1d 3971 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ((abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
15 | 11, 14 | imbi12d 233 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ((((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
16 | 15 | ralbidv 2454 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐴 → (∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
17 | 16 | rspcv 2809 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
18 | 17 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
19 | | subid 8073 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) |
20 | 19 | ad2antrr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 − 𝐴) = 0) |
21 | 20 | abs00bd 10943 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) = 0) |
22 | | simprll 527 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑡 ∈ ℝ+) |
23 | 22 | rpgt0d 9584 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 0 < 𝑡) |
24 | 21, 23 | eqbrtrd 3982 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) < 𝑡) |
25 | 24 | biantrurd 303 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘(𝑢 − 𝑦)) < 𝑤 ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
26 | | simprr 522 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑢 ∈ ℂ) |
27 | | simpll 519 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝐴 ∈ ℂ) |
28 | 27, 26 | mulcld 7877 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 · 𝑢) ∈ ℂ) |
29 | | oveq2 5822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) |
30 | 29, 2 | fvmptg 5537 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℂ ∧ (𝐴 · 𝑢) ∈ ℂ) → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
31 | 26, 28, 30 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
32 | | simplrl 525 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑦 ∈ ℂ) |
33 | 27, 32 | mulcld 7877 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 · 𝑦) ∈ ℂ) |
34 | | oveq2 5822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
35 | 34, 2 | fvmptg 5537 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℂ ∧ (𝐴 · 𝑦) ∈ ℂ) → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
36 | 32, 33, 35 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
37 | 31, 36 | oveq12d 5832 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((𝐹‘𝑢) − (𝐹‘𝑦)) = ((𝐴 · 𝑢) − (𝐴 · 𝑦))) |
38 | 37 | fveq2d 5465 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
39 | 38 | breq1d 3971 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
40 | 25, 39 | imbi12d 233 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
41 | 40 | anassrs 398 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) ∧ 𝑢 ∈ ℂ) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
42 | 41 | ralbidva 2450 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
43 | 18, 42 | sylibrd 168 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
44 | 43 | anassrs 398 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) ∧ 𝑤 ∈ ℝ+) →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
45 | 44 | reximdva 2556 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
46 | 45 | rexlimdva 2571 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ (∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
47 | 8, 46 | mpd 13 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
48 | 47 | ralrimivva 2536 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈ ℂ
∀𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
49 | | ssid 3144 |
. . 3
⊢ ℂ
⊆ ℂ |
50 | | elcncf2 12900 |
. . 3
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)))) |
51 | 49, 49, 50 | mp2an 423 |
. 2
⊢ (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
52 | 3, 48, 51 | sylanbrc 414 |
1
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |