Theorem expcncf

Description: The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn . (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Assertion	expcncf	|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
2	1	expcn	|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
3	1	cncfcn1	|- ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
4	2 3	eleqtrrdi	|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )