Theorem efcn

Description: The exponential function is continuous. (Contributed by Paul Chapman, 15-Sep-2007) (Revised by Mario Carneiro, 20-Jun-2015)

	Ref	Expression
Assertion	efcn	$$⊢\exp :ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢ℂ\subseteq ℂ$$
2		eff	$$⊢\exp :ℂ⟶ℂ$$
3		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
4	3	feq1i	$$⊢{\exp }_{ℂ}^{\prime }:ℂ⟶ℂ\leftrightarrow \exp :ℂ⟶ℂ$$
5	2 4	mpbir	$$⊢{\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
6	5	fdmi	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }=ℂ$$
7		dvcn	$$⊢\left(\left(ℂ\subseteq ℂ\wedge \exp :ℂ⟶ℂ\wedge ℂ\subseteq ℂ\right)\wedge \mathrm{dom}{\exp }_{ℂ}^{\prime }=ℂ\right)\to \exp :ℂ\underset{cn}{⟶}ℂ$$
8	6 7	mpan2	$$⊢\left(ℂ\subseteq ℂ\wedge \exp :ℂ⟶ℂ\wedge ℂ\subseteq ℂ\right)\to \exp :ℂ\underset{cn}{⟶}ℂ$$
9	1 2 1 8	mp3an	$$⊢\exp :ℂ\underset{cn}{⟶}ℂ$$