# Metamath Proof Explorer

## Theorem recncf

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

Ref Expression
Assertion recncf ${⊢}\Re :ℂ\underset{cn}{⟶}ℝ$

### Proof

Step Hyp Ref Expression
1 ref ${⊢}\Re :ℂ⟶ℝ$
2 recn2 ${⊢}\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|\Re \left({w}\right)-\Re \left({x}\right)\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|\Re \left({w}\right)-\Re \left({x}\right)\right|<{y}\right)$
4 ssid ${⊢}ℂ\subseteq ℂ$
5 ax-resscn ${⊢}ℝ\subseteq ℂ$
6 elcncf2 ${⊢}\left(ℂ\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to \left(\Re :ℂ\underset{cn}{⟶}ℝ↔\left(\Re :ℂ⟶ℝ\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|\Re \left({w}\right)-\Re \left({x}\right)\right|<{y}\right)\right)\right)$
7 4 5 6 mp2an ${⊢}\Re :ℂ\underset{cn}{⟶}ℝ↔\left(\Re :ℂ⟶ℝ\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|\Re \left({w}\right)-\Re \left({x}\right)\right|<{y}\right)\right)$
8 1 3 7 mpbir2an ${⊢}\Re :ℂ\underset{cn}{⟶}ℝ$