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 ∈ ( ℂ –cn→ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℂ ⊆ ℂ
2		eff	⊢ exp : ℂ ⟶ ℂ
3		dvef	⊢ ( ℂ D exp ) = exp
4	3	feq1i	⊢ ( ( ℂ D exp ) : ℂ ⟶ ℂ ↔ exp : ℂ ⟶ ℂ )
5	2 4	mpbir	⊢ ( ℂ D exp ) : ℂ ⟶ ℂ
6	5	fdmi	⊢ dom ( ℂ D exp ) = ℂ
7		dvcn	⊢ ( ( ( ℂ ⊆ ℂ ∧ exp : ℂ ⟶ ℂ ∧ ℂ ⊆ ℂ ) ∧ dom ( ℂ D exp ) = ℂ ) → exp ∈ ( ℂ –cn→ ℂ ) )
8	6 7	mpan2	⊢ ( ( ℂ ⊆ ℂ ∧ exp : ℂ ⟶ ℂ ∧ ℂ ⊆ ℂ ) → exp ∈ ( ℂ –cn→ ℂ ) )
9	1 2 1 8	mp3an	⊢ exp ∈ ( ℂ –cn→ ℂ )