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 e. ( CC -cn-> CC )

Proof

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 )