# Metamath Proof Explorer

## Theorem cjcn2

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

Ref Expression
Assertion cjcn2 ${⊢}\left({A}\in ℂ\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{A}\right|<{y}\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|<{x}\right)$

### Proof

Step Hyp Ref Expression
1 cjf ${⊢}*:ℂ⟶ℂ$
2 cjcl ${⊢}{z}\in ℂ\to \stackrel{‾}{{z}}\in ℂ$
3 cjcl ${⊢}{A}\in ℂ\to \stackrel{‾}{{A}}\in ℂ$
4 subcl ${⊢}\left(\stackrel{‾}{{z}}\in ℂ\wedge \stackrel{‾}{{A}}\in ℂ\right)\to \stackrel{‾}{{z}}-\stackrel{‾}{{A}}\in ℂ$
5 2 3 4 syl2an ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \stackrel{‾}{{z}}-\stackrel{‾}{{A}}\in ℂ$
6 5 abscld ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|\in ℝ$
7 cjsub ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \stackrel{‾}{{z}-{A}}=\stackrel{‾}{{z}}-\stackrel{‾}{{A}}$
8 7 fveq2d ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left|\stackrel{‾}{{z}-{A}}\right|=\left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|$
9 subcl ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to {z}-{A}\in ℂ$
10 9 abscjd ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left|\stackrel{‾}{{z}-{A}}\right|=\left|{z}-{A}\right|$
11 8 10 eqtr3d ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|=\left|{z}-{A}\right|$
12 6 11 eqled ${⊢}\left({z}\in ℂ\wedge {A}\in ℂ\right)\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|\le \left|{z}-{A}\right|$
13 1 12 cn1lem ${⊢}\left({A}\in ℂ\wedge {x}\in {ℝ}^{+}\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {z}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{z}-{A}\right|<{y}\to \left|\stackrel{‾}{{z}}-\stackrel{‾}{{A}}\right|<{x}\right)$