cjcn2

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

		Ref	Expression
	Assertion	cjcn2	$⊢ (A \in ℂ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in ℂ (\|z - A\| < y \to \|\overline{z} - \overline{A}\| < x)$

Step	Hyp	Ref	Expression
1		cjf	$⊢ * : ℂ ⟶ ℂ$
2		cjcl	$⊢ z \in ℂ \to \overline{z} \in ℂ$
3		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
4		subcl	$⊢ (\overline{z} \in ℂ \land \overline{A} \in ℂ) \to \overline{z} - \overline{A} \in ℂ$
5	2 3 4	syl2an	$⊢ (z \in ℂ \land A \in ℂ) \to \overline{z} - \overline{A} \in ℂ$
6	5	abscld	$⊢ (z \in ℂ \land A \in ℂ) \to \|\overline{z} - \overline{A}\| \in ℝ$
7		cjsub	$⊢ (z \in ℂ \land A \in ℂ) \to \overline{z - A} = \overline{z} - \overline{A}$
8	7	fveq2d	$⊢ (z \in ℂ \land A \in ℂ) \to \|\overline{z - A}\| = \|\overline{z} - \overline{A}\|$
9		subcl	$⊢ (z \in ℂ \land A \in ℂ) \to z - A \in ℂ$
10	9	abscjd	$⊢ (z \in ℂ \land A \in ℂ) \to \|\overline{z - A}\| = \|z - A\|$
11	8 10	eqtr3d	$⊢ (z \in ℂ \land A \in ℂ) \to \|\overline{z} - \overline{A}\| = \|z - A\|$
12	6 11	eqled	$⊢ (z \in ℂ \land A \in ℂ) \to \|\overline{z} - \overline{A}\| \leq \|z - A\|$
13	1 12	cn1lem	$⊢ (A \in ℂ \land x \in ℝ^{+}) \to \exists y \in ℝ^{+} \forall z \in ℂ (\|z - A\| < y \to \|\overline{z} - \overline{A}\| < x)$

Metamath Proof Explorer