| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mulcl 11240 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 · 𝑥) ∈ ℂ) | 
| 2 |  | mulc1cncf.1 | . . 3
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) | 
| 3 | 1, 2 | fmptd 7133 | . 2
⊢ (𝐴 ∈ ℂ → 𝐹:ℂ⟶ℂ) | 
| 4 |  | simprr 772 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑧 ∈
ℝ+) | 
| 5 |  | simpl 482 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝐴 ∈
ℂ) | 
| 6 |  | simprl 770 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ 𝑦 ∈
ℂ) | 
| 7 |  | mulcn2 15633 | . . . . 5
⊢ ((𝑧 ∈ ℝ+
∧ 𝐴 ∈ ℂ
∧ 𝑦 ∈ ℂ)
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) | 
| 8 | 4, 5, 6, 7 | syl3anc 1372 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) | 
| 9 |  | fvoveq1 7455 | . . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (abs‘(𝑣 − 𝐴)) = (abs‘(𝐴 − 𝐴))) | 
| 10 | 9 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → ((abs‘(𝑣 − 𝐴)) < 𝑡 ↔ (abs‘(𝐴 − 𝐴)) < 𝑡)) | 
| 11 | 10 | anbi1d 631 | . . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) | 
| 12 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑣 = 𝐴 → (𝑣 · 𝑢) = (𝐴 · 𝑢)) | 
| 13 | 12 | fvoveq1d 7454 | . . . . . . . . . . . . 13
⊢ (𝑣 = 𝐴 → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) | 
| 14 | 13 | breq1d 5152 | . . . . . . . . . . . 12
⊢ (𝑣 = 𝐴 → ((abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) | 
| 15 | 11, 14 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑣 = 𝐴 → ((((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 16 | 15 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑣 = 𝐴 → (∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 17 | 16 | rspcv 3617 | . . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 18 | 17 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 19 |  | subid 11529 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℂ → (𝐴 − 𝐴) = 0) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐴 − 𝐴) = 0) | 
| 21 | 20 | abs00bd 15331 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) = 0) | 
| 22 |  | simprll 778 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑡 ∈ ℝ+) | 
| 23 | 22 | rpgt0d 13081 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 0 < 𝑡) | 
| 24 | 21, 23 | eqbrtrd 5164 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘(𝐴 − 𝐴)) < 𝑡) | 
| 25 | 24 | biantrurd 532 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘(𝑢 − 𝑦)) < 𝑤 ↔ ((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤))) | 
| 26 |  | simprr 772 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑢 ∈ ℂ) | 
| 27 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (𝐴 · 𝑥) = (𝐴 · 𝑢)) | 
| 28 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑢) ∈ V | 
| 29 | 27, 2, 28 | fvmpt 7015 | . . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ℂ → (𝐹‘𝑢) = (𝐴 · 𝑢)) | 
| 30 | 26, 29 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑢) = (𝐴 · 𝑢)) | 
| 31 |  | simplrl 776 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → 𝑦 ∈ ℂ) | 
| 32 |  | oveq2 7440 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) | 
| 33 |  | ovex 7465 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 · 𝑦) ∈ V | 
| 34 | 32, 2, 33 | fvmpt 7015 | . . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℂ → (𝐹‘𝑦) = (𝐴 · 𝑦)) | 
| 35 | 31, 34 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (𝐹‘𝑦) = (𝐴 · 𝑦)) | 
| 36 | 30, 35 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((𝐹‘𝑢) − (𝐹‘𝑦)) = ((𝐴 · 𝑢) − (𝐴 · 𝑦))) | 
| 37 | 36 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) = (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦)))) | 
| 38 | 37 | breq1d 5152 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → ((abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧 ↔ (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧)) | 
| 39 | 25, 38 | imbi12d 344 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ ((𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+) ∧ 𝑢 ∈ ℂ)) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 40 | 39 | anassrs 467 | . . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) ∧ 𝑢 ∈ ℂ) → (((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 41 | 40 | ralbidva 3175 | . . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧) ↔ ∀𝑢 ∈ ℂ (((abs‘(𝐴 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝐴 · 𝑢) − (𝐴 · 𝑦))) < 𝑧))) | 
| 42 | 18, 41 | sylibrd 259 | . . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ (𝑡 ∈
ℝ+ ∧ 𝑤
∈ ℝ+)) → (∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ (((abs‘(𝑣 − 𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) | 
| 43 | 42 | anassrs 467 | . . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) ∧ 𝑤 ∈ ℝ+) →
(∀𝑣 ∈ ℂ
∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) | 
| 44 | 43 | reximdva 3167 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
∧ 𝑡 ∈
ℝ+) → (∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) | 
| 45 | 44 | rexlimdva 3154 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ (∃𝑡 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑣 ∈ ℂ ∀𝑢 ∈ ℂ
(((abs‘(𝑣 −
𝐴)) < 𝑡 ∧ (abs‘(𝑢 − 𝑦)) < 𝑤) → (abs‘((𝑣 · 𝑢) − (𝐴 · 𝑦))) < 𝑧) → ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) | 
| 46 | 8, 45 | mpd 15 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ (𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+))
→ ∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) | 
| 47 | 46 | ralrimivva 3201 | . 2
⊢ (𝐴 ∈ ℂ →
∀𝑦 ∈ ℂ
∀𝑧 ∈
ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)) | 
| 48 |  | ssid 4005 | . . 3
⊢ ℂ
⊆ ℂ | 
| 49 |  | elcncf2 24917 | . . 3
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧)))) | 
| 50 | 48, 48, 49 | mp2an 692 | . 2
⊢ (𝐹 ∈ (ℂ–cn→ℂ) ↔ (𝐹:ℂ⟶ℂ ∧ ∀𝑦 ∈ ℂ ∀𝑧 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − 𝑦)) < 𝑤 → (abs‘((𝐹‘𝑢) − (𝐹‘𝑦))) < 𝑧))) | 
| 51 | 3, 47, 50 | sylanbrc 583 | 1
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) |