# Metamath Proof Explorer

## Theorem cjcncf

Description: Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion cjcncf ${⊢}*:ℂ\underset{cn}{⟶}ℂ$

### Proof

Step Hyp Ref Expression
1 cjf ${⊢}*:ℂ⟶ℂ$
2 cjcn2 ${⊢}\left({x}\in ℂ\wedge {y}\in {ℝ}^{+}\right)\to \exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|\stackrel{‾}{{w}}-\stackrel{‾}{{x}}\right|<{y}\right)$
3 2 rgen2 ${⊢}\forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|\stackrel{‾}{{w}}-\stackrel{‾}{{x}}\right|<{y}\right)$
4 ssid ${⊢}ℂ\subseteq ℂ$
5 elcncf2 ${⊢}\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(*:ℂ\underset{cn}{⟶}ℂ↔\left(*:ℂ⟶ℂ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|\stackrel{‾}{{w}}-\stackrel{‾}{{x}}\right|<{y}\right)\right)\right)$
6 4 4 5 mp2an ${⊢}*:ℂ\underset{cn}{⟶}ℂ↔\left(*:ℂ⟶ℂ\wedge \forall {x}\in ℂ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℂ\phantom{\rule{.4em}{0ex}}\left(\left|{w}-{x}\right|<{z}\to \left|\stackrel{‾}{{w}}-\stackrel{‾}{{x}}\right|<{y}\right)\right)$
7 1 3 6 mpbir2an ${⊢}*:ℂ\underset{cn}{⟶}ℂ$