Step | Hyp | Ref
| Expression |
1 | | mulcl 10699 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) |
2 | | mulc1cncf.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) |
3 | 1, 2 | fmptd 6888 |
. 2
⊢ (𝐴 ∈ ℂ → 𝐹:ℂ⟶ℂ) |
4 | | simprr 773 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑧 ∈
ℝ+) |
5 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝐴 ∈
ℂ) |
6 | | simprl 771 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑦 ∈
ℂ) |
7 | | mulcn2 15043 |
. . . . 5
⊢ ((𝑧 ∈ ℝ+
∧ 𝐴 ∈ ℂ
∧ 𝑦 ∈ ℂ)
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
9 | | fvoveq1 7193 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (abs‘(𝑣 − 𝐴)) = (abs‘(𝐴 − 𝐴))) |
10 | 9 | breq1d 5040 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → ((abs‘(𝑣 − 𝐴)) < 𝑡 ↔ (abs‘(𝐴 − 𝐴)) < 𝑡)) |
11 | 10 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
12 | | oveq1 7177 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (𝑣 · 𝑢) = (𝐴 · 𝑢)) |
13 | 12 | fvoveq1d 7192 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
14 | 13 | breq1d 5040 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ((abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
15 | 11, 14 | imbi12d 348 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ((((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
16 | 15 | ralbidv 3109 |
. . . . . . . . . 10
⊢ (𝑣 = 𝐴 → (∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
17 | 16 | rspcv 3521 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
18 | 17 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
19 | | subid 10983 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) |
20 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 − 𝐴) = 0) |
21 | 20 | abs00bd 14741 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) = 0) |
22 | | simprll 779 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑡 ∈ ℝ+) |
23 | 22 | rpgt0d 12517 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 0 < 𝑡) |
24 | 21, 23 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) < 𝑡) |
25 | 24 | biantrurd 536 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘(𝑢 − 𝑦)) < 𝑤 ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) |
26 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑢 ∈ ℂ) |
27 | | oveq2 7178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) |
28 | | ovex 7203 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑢) ∈ V |
29 | 27, 2, 28 | fvmpt 6775 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
30 | 26, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑢) = (𝐴 · 𝑢)) |
31 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑦 ∈ ℂ) |
32 | | oveq2 7178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
33 | | ovex 7203 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑦) ∈ V |
34 | 32, 2, 33 | fvmpt 6775 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
35 | 31, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑦) = (𝐴 · 𝑦)) |
36 | 30, 35 | oveq12d 7188 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((𝐹‘𝑢) − (𝐹‘𝑦)) = ((𝐴 · 𝑢) − (𝐴 · 𝑦))) |
37 | 36 | fveq2d 6678 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) |
38 | 37 | breq1d 5040 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) |
39 | 25, 38 | imbi12d 348 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
40 | 39 | anassrs 471 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) ∧ 𝑢 ∈ ℂ) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
41 | 40 | ralbidva 3108 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) |
42 | 18, 41 | sylibrd 262 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
43 | 42 | anassrs 471 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) ∧ 𝑤 ∈ ℝ+) →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
44 | 43 | reximdva 3184 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
45 | 44 | rexlimdva 3194 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ (∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
46 | 8, 45 | mpd 15 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
47 | 46 | ralrimivva 3103 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈ ℂ
∀𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) |
48 | | ssid 3899 |
. . 3
⊢ ℂ
⊆ ℂ |
49 | | elcncf2 23642 |
. . 3
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)))) |
50 | 48, 48, 49 | mp2an 692 |
. 2
⊢ (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) |
51 | 3, 47, 50 | sylanbrc 586 |
1
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |