Step |
Hyp |
Ref |
Expression |
1 |
|
cn1lem.1 |
⊢ 𝐹 : ℂ ⟶ ℂ |
2 |
|
cn1lem.2 |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ) |
3 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ ) |
4 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ ) |
5 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ ) |
6 |
4 5 2
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ) |
7 |
1
|
ffvelrni |
⊢ ( 𝑧 ∈ ℂ → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
8 |
4 7
|
syl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ ) |
9 |
1
|
ffvelrni |
⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ‘ 𝐴 ) ∈ ℂ ) |
10 |
5 9
|
syl |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ ) |
11 |
8 10
|
subcld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ∈ ℂ ) |
12 |
11
|
abscld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ ) |
13 |
4 5
|
subcld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 − 𝐴 ) ∈ ℂ ) |
14 |
13
|
abscld |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 𝐴 ) ) ∈ ℝ ) |
15 |
|
rpre |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ ) |
16 |
15
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → 𝑥 ∈ ℝ ) |
17 |
|
lelttr |
⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ∈ ℝ ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |
18 |
12 14 16 17
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ∧ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |
19 |
6 18
|
mpand |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |
20 |
19
|
ralrimiva |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |
21 |
|
breq2 |
⊢ ( 𝑦 = 𝑥 → ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 ↔ ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 ) ) |
22 |
21
|
rspceaimv |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |
23 |
3 20 22
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) ) |