Metamath Proof Explorer


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→ ℂ )