# Metamath Proof Explorer

## Theorem expcn

Description: The power function on complex numbers, for fixed exponent N , is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypothesis expcn.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion expcn ${⊢}{N}\in {ℕ}_{0}\to \left({x}\in ℂ⟼{{x}}^{{N}}\right)\in \left({J}\mathrm{Cn}{J}\right)$

### Proof

Step Hyp Ref Expression
1 expcn.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 oveq2 ${⊢}{n}=0\to {{x}}^{{n}}={{x}}^{0}$
3 2 mpteq2dv ${⊢}{n}=0\to \left({x}\in ℂ⟼{{x}}^{{n}}\right)=\left({x}\in ℂ⟼{{x}}^{0}\right)$
4 3 eleq1d ${⊢}{n}=0\to \left(\left({x}\in ℂ⟼{{x}}^{{n}}\right)\in \left({J}\mathrm{Cn}{J}\right)↔\left({x}\in ℂ⟼{{x}}^{0}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)$
5 oveq2 ${⊢}{n}={k}\to {{x}}^{{n}}={{x}}^{{k}}$
6 5 mpteq2dv ${⊢}{n}={k}\to \left({x}\in ℂ⟼{{x}}^{{n}}\right)=\left({x}\in ℂ⟼{{x}}^{{k}}\right)$
7 6 eleq1d ${⊢}{n}={k}\to \left(\left({x}\in ℂ⟼{{x}}^{{n}}\right)\in \left({J}\mathrm{Cn}{J}\right)↔\left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)$
8 oveq2 ${⊢}{n}={k}+1\to {{x}}^{{n}}={{x}}^{{k}+1}$
9 8 mpteq2dv ${⊢}{n}={k}+1\to \left({x}\in ℂ⟼{{x}}^{{n}}\right)=\left({x}\in ℂ⟼{{x}}^{{k}+1}\right)$
10 9 eleq1d ${⊢}{n}={k}+1\to \left(\left({x}\in ℂ⟼{{x}}^{{n}}\right)\in \left({J}\mathrm{Cn}{J}\right)↔\left({x}\in ℂ⟼{{x}}^{{k}+1}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)$
11 oveq2 ${⊢}{n}={N}\to {{x}}^{{n}}={{x}}^{{N}}$
12 11 mpteq2dv ${⊢}{n}={N}\to \left({x}\in ℂ⟼{{x}}^{{n}}\right)=\left({x}\in ℂ⟼{{x}}^{{N}}\right)$
13 12 eleq1d ${⊢}{n}={N}\to \left(\left({x}\in ℂ⟼{{x}}^{{n}}\right)\in \left({J}\mathrm{Cn}{J}\right)↔\left({x}\in ℂ⟼{{x}}^{{N}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)$
14 exp0 ${⊢}{x}\in ℂ\to {{x}}^{0}=1$
15 14 mpteq2ia ${⊢}\left({x}\in ℂ⟼{{x}}^{0}\right)=\left({x}\in ℂ⟼1\right)$
16 1 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
17 16 a1i ${⊢}\top \to {J}\in \mathrm{TopOn}\left(ℂ\right)$
18 1cnd ${⊢}\top \to 1\in ℂ$
19 17 17 18 cnmptc ${⊢}\top \to \left({x}\in ℂ⟼1\right)\in \left({J}\mathrm{Cn}{J}\right)$
20 19 mptru ${⊢}\left({x}\in ℂ⟼1\right)\in \left({J}\mathrm{Cn}{J}\right)$
21 15 20 eqeltri ${⊢}\left({x}\in ℂ⟼{{x}}^{0}\right)\in \left({J}\mathrm{Cn}{J}\right)$
22 oveq1 ${⊢}{x}={n}\to {{x}}^{{k}+1}={{n}}^{{k}+1}$
23 22 cbvmptv ${⊢}\left({x}\in ℂ⟼{{x}}^{{k}+1}\right)=\left({n}\in ℂ⟼{{n}}^{{k}+1}\right)$
24 id ${⊢}{n}\in ℂ\to {n}\in ℂ$
25 simpl ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to {k}\in {ℕ}_{0}$
26 expp1 ${⊢}\left({n}\in ℂ\wedge {k}\in {ℕ}_{0}\right)\to {{n}}^{{k}+1}={{n}}^{{k}}{n}$
27 24 25 26 syl2anr ${⊢}\left(\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\wedge {n}\in ℂ\right)\to {{n}}^{{k}+1}={{n}}^{{k}}{n}$
28 27 mpteq2dva ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({n}\in ℂ⟼{{n}}^{{k}+1}\right)=\left({n}\in ℂ⟼{{n}}^{{k}}{n}\right)$
29 23 28 syl5eq ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({x}\in ℂ⟼{{x}}^{{k}+1}\right)=\left({n}\in ℂ⟼{{n}}^{{k}}{n}\right)$
30 16 a1i ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to {J}\in \mathrm{TopOn}\left(ℂ\right)$
31 oveq1 ${⊢}{x}={n}\to {{x}}^{{k}}={{n}}^{{k}}$
32 31 cbvmptv ${⊢}\left({x}\in ℂ⟼{{x}}^{{k}}\right)=\left({n}\in ℂ⟼{{n}}^{{k}}\right)$
33 simpr ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)$
34 32 33 eqeltrrid ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({n}\in ℂ⟼{{n}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)$
35 30 cnmptid ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({n}\in ℂ⟼{n}\right)\in \left({J}\mathrm{Cn}{J}\right)$
36 1 mulcn ${⊢}×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
37 36 a1i ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to ×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
38 30 34 35 37 cnmpt12f ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({n}\in ℂ⟼{{n}}^{{k}}{n}\right)\in \left({J}\mathrm{Cn}{J}\right)$
39 29 38 eqeltrd ${⊢}\left({k}\in {ℕ}_{0}\wedge \left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)\to \left({x}\in ℂ⟼{{x}}^{{k}+1}\right)\in \left({J}\mathrm{Cn}{J}\right)$
40 39 ex ${⊢}{k}\in {ℕ}_{0}\to \left(\left({x}\in ℂ⟼{{x}}^{{k}}\right)\in \left({J}\mathrm{Cn}{J}\right)\to \left({x}\in ℂ⟼{{x}}^{{k}+1}\right)\in \left({J}\mathrm{Cn}{J}\right)\right)$
41 4 7 10 13 21 40 nn0ind ${⊢}{N}\in {ℕ}_{0}\to \left({x}\in ℂ⟼{{x}}^{{N}}\right)\in \left({J}\mathrm{Cn}{J}\right)$