This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
2	1	expcn	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ( TopOpen ‘ ℂ_fld ) Cn ( TopOpen ‘ ℂ_fld ) ) )
3	1	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂ_fld ) Cn ( TopOpen ‘ ℂ_fld ) )
4	2 3	eleqtrrdi	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )