Metamath Proof Explorer

Theorem cjcn2

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

Ref Expression
Assertion cjcn2 ⊢ A ∈ ℂ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − A < y → z ‾ − A ‾ < x

Proof

Step Hyp Ref Expression
1 cjf ⊢ * : ℂ ⟶ ℂ
2 cjcl ⊢ z ∈ ℂ → z ‾ ∈ ℂ
3 cjcl ⊢ A ∈ ℂ → A ‾ ∈ ℂ
4 subcl ⊢ z ‾ ∈ ℂ ∧ A ‾ ∈ ℂ → z ‾ − A ‾ ∈ ℂ
5 2 3 4 syl2an ⊢ z ∈ ℂ ∧ A ∈ ℂ → z ‾ − A ‾ ∈ ℂ
6 5 abscld ⊢ z ∈ ℂ ∧ A ∈ ℂ → z ‾ − A ‾ ∈ ℝ
7 cjsub ⊢ z ∈ ℂ ∧ A ∈ ℂ → z − A ‾ = z ‾ − A ‾
8 7 fveq2d ⊢ z ∈ ℂ ∧ A ∈ ℂ → z − A ‾ = z ‾ − A ‾
9 subcl ⊢ z ∈ ℂ ∧ A ∈ ℂ → z − A ∈ ℂ
10 9 abscjd ⊢ z ∈ ℂ ∧ A ∈ ℂ → z − A ‾ = z − A
11 8 10 eqtr3d ⊢ z ∈ ℂ ∧ A ∈ ℂ → z ‾ − A ‾ = z − A
12 6 11 eqled ⊢ z ∈ ℂ ∧ A ∈ ℂ → z ‾ − A ‾ ≤ z − A
13 1 12 cn1lem ⊢ A ∈ ℂ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − A < y → z ‾ − A ‾ < x