Theorem abscn2

Description: The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Assertion	abscn2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝐴 ) ) ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		absf	⊢ abs : ℂ ⟶ ℝ
2		ax-resscn	⊢ ℝ ⊆ ℂ
3		fss	⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → abs : ℂ ⟶ ℂ )
4	1 2 3	mp2an	⊢ abs : ℂ ⟶ ℂ
5		abs2difabs	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) )
6	4 5	cn1lem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( abs ‘ 𝑧 ) − ( abs ‘ 𝐴 ) ) ) < 𝑥 ) )