Metamath Proof Explorer
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→ ℂ ) |