Metamath Proof Explorer

Theorem cn1lem

Description: A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses cn1lem.1 ⊢ 𝐹 : ℂ ⟶ ℂ
cn1lem.2 ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) )
Assertion cn1lem ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )

Proof

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 ffvelcdmi ⊢ ( 𝑧 ∈ ℂ → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
8 4 7 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑧 ∈ ℂ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
9 1 ffvelcdmi ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ‘ 𝐴 ) ∈ ℂ )
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 ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐴 ) ) ) < 𝑥 ) )