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 e. ( CC -cn-> CC ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | |- CC C_ CC |
|
2 | eff | |- exp : CC --> CC |
|
3 | dvef | |- ( CC _D exp ) = exp |
|
4 | 3 | feq1i | |- ( ( CC _D exp ) : CC --> CC <-> exp : CC --> CC ) |
5 | 2 4 | mpbir | |- ( CC _D exp ) : CC --> CC |
6 | 5 | fdmi | |- dom ( CC _D exp ) = CC |
7 | dvcn | |- ( ( ( CC C_ CC /\ exp : CC --> CC /\ CC C_ CC ) /\ dom ( CC _D exp ) = CC ) -> exp e. ( CC -cn-> CC ) ) |
|
8 | 6 7 | mpan2 | |- ( ( CC C_ CC /\ exp : CC --> CC /\ CC C_ CC ) -> exp e. ( CC -cn-> CC ) ) |
9 | 1 2 1 8 | mp3an | |- exp e. ( CC -cn-> CC ) |