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=TopOpen⁡ℂfld
Assertion expcn ⊢N∈ℕ0→x∈ℂ⟼xN∈JCnJ

Proof

Step Hyp Ref Expression
1 expcn.j ⊢J=TopOpen⁡ℂfld
2 oveq2 ⊢n=0→xn=x0
3 2 mpteq2dv ⊢n=0→x∈ℂ⟼xn=x∈ℂ⟼x0
4 3 eleq1d ⊢n=0→x∈ℂ⟼xn∈JCnJ↔x∈ℂ⟼x0∈JCnJ
5 oveq2 ⊢n=k→xn=xk
6 5 mpteq2dv ⊢n=k→x∈ℂ⟼xn=x∈ℂ⟼xk
7 6 eleq1d ⊢n=k→x∈ℂ⟼xn∈JCnJ↔x∈ℂ⟼xk∈JCnJ
8 oveq2 ⊢n=k+1→xn=xk+1
9 8 mpteq2dv ⊢n=k+1→x∈ℂ⟼xn=x∈ℂ⟼xk+1
10 9 eleq1d ⊢n=k+1→x∈ℂ⟼xn∈JCnJ↔x∈ℂ⟼xk+1∈JCnJ
11 oveq2 ⊢n=N→xn=xN
12 11 mpteq2dv ⊢n=N→x∈ℂ⟼xn=x∈ℂ⟼xN
13 12 eleq1d ⊢n=N→x∈ℂ⟼xn∈JCnJ↔x∈ℂ⟼xN∈JCnJ
14 exp0 ⊢x∈ℂ→x0=1
15 14 mpteq2ia ⊢x∈ℂ⟼x0=x∈ℂ⟼1
16 1 cnfldtopon ⊢J∈TopOn⁡ℂ
17 16 a1i ⊢⊤→J∈TopOn⁡ℂ
18 1cnd ⊢⊤→1∈ℂ
19 17 17 18 cnmptc ⊢⊤→x∈ℂ⟼1∈JCnJ
20 19 mptru ⊢x∈ℂ⟼1∈JCnJ
21 15 20 eqeltri ⊢x∈ℂ⟼x0∈JCnJ
22 oveq1 ⊢x=n→xk+1=nk+1
23 22 cbvmptv ⊢x∈ℂ⟼xk+1=n∈ℂ⟼nk+1
24 id ⊢n∈ℂ→n∈ℂ
25 simpl ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→k∈ℕ0
26 expp1 ⊢n∈ℂ∧k∈ℕ0→nk+1=nk⁢n
27 24 25 26 syl2anr ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ∧n∈ℂ→nk+1=nk⁢n
28 27 mpteq2dva ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→n∈ℂ⟼nk+1=n∈ℂ⟼nk⁢n
29 23 28 eqtrid ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→x∈ℂ⟼xk+1=n∈ℂ⟼nk⁢n
30 16 a1i ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→J∈TopOn⁡ℂ
31 oveq1 ⊢x=n→xk=nk
32 31 cbvmptv ⊢x∈ℂ⟼xk=n∈ℂ⟼nk
33 simpr ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→x∈ℂ⟼xk∈JCnJ
34 32 33 eqeltrrid ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→n∈ℂ⟼nk∈JCnJ
35 30 cnmptid ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→n∈ℂ⟼n∈JCnJ
36 1 mulcn ⊢×∈J×tJCnJ
37 36 a1i ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→×∈J×tJCnJ
38 30 34 35 37 cnmpt12f ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→n∈ℂ⟼nk⁢n∈JCnJ
39 29 38 eqeltrd ⊢k∈ℕ0∧x∈ℂ⟼xk∈JCnJ→x∈ℂ⟼xk+1∈JCnJ
40 39 ex ⊢k∈ℕ0→x∈ℂ⟼xk∈JCnJ→x∈ℂ⟼xk+1∈JCnJ
41 4 7 10 13 21 40 nn0ind ⊢N∈ℕ0→x∈ℂ⟼xN∈JCnJ