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 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 ‘ ( ( 𝐹𝑧 ) − ( 𝐹𝐴 ) ) ) < 𝑥 ) )