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\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^N\right):ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	expcn	$$⊢N\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^N\right)\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
3	1	cncfcn1	$$⊢ℂ\underset{cn}{⟶}ℂ=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
4	2 3	eleqtrrdi	$$⊢N\in {\mathbb{N}}_0\to \left(x\in ℂ⟼x^N\right):ℂ\underset{cn}{⟶}ℂ$$