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 ⊢ N ∈ ℕ 0 → x ∈ ℂ ⟼ x N : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
2 1 expcn ⊢ N ∈ ℕ 0 → x ∈ ℂ ⟼ x N ∈ TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
3 1 cncfcn1 ⊢ ℂ ⟶cn ℂ = TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
4 2 3 eleqtrrdi ⊢ N ∈ ℕ 0 → x ∈ ℂ ⟼ x N : ℂ ⟶cn ℂ