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 )