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

Proof

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