This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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