Database
BASIC TOPOLOGY
Metric spaces
Topological definitions using the reals
expcncf
Metamath Proof Explorer
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 → ℂ ) )