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) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis expcn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion expcn ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 expcn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 0 ) )
3 2 mpteq2dv ⊢ ( 𝑛 = 0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 0 ) ) )
4 3 eleq1d ⊢ ( 𝑛 = 0 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 0 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
5 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑘 ) )
6 5 mpteq2dv ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) )
7 6 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
8 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ ( 𝑘 + 1 ) ) )
9 8 mpteq2dv ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) )
10 9 eleq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
11 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑁 ) )
12 11 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) )
13 12 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
14 exp0 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑ 0 ) = 1 )
15 14 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 0 ) ) = ( 𝑥 ∈ ℂ ↦ 1 )
16 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
17 16 a1i ⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
18 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
19 17 17 18 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( 𝐽 Cn 𝐽 ) )
20 19 mptru ⊢ ( 𝑥 ∈ ℂ ↦ 1 ) ∈ ( 𝐽 Cn 𝐽 )
21 15 20 eqeltri ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 0 ) ) ∈ ( 𝐽 Cn 𝐽 )
22 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ ( 𝑘 + 1 ) ) = ( 𝑛 ↑ ( 𝑘 + 1 ) ) )
23 22 cbvmptv ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ ( 𝑘 + 1 ) ) )
24 id ⊢ ( 𝑛 ∈ ℂ → 𝑛 ∈ ℂ )
25 simpl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → 𝑘 ∈ ℕ0 )
26 expp1 ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑛 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) )
27 expcl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑛 ↑ 𝑘 ) ∈ ℂ )
28 simpl ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → 𝑛 ∈ ℂ )
29 ovmpot ⊢ ( ( ( 𝑛 ↑ 𝑘 ) ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) = ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) )
30 27 28 29 syl2anc ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) = ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) )
31 26 30 eqtr4d ⊢ ( ( 𝑛 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑛 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) )
32 24 25 31 syl2anr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑛 ∈ ℂ ) → ( 𝑛 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) )
33 32 mpteq2dva ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) ) )
34 23 33 eqtrid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) ) )
35 16 a1i ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
36 oveq1 ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ 𝑘 ) = ( 𝑛 ↑ 𝑘 ) )
37 36 cbvmptv ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) = ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ 𝑘 ) )
38 simpr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
39 37 38 eqeltrrid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
40 35 cnmptid ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ 𝑛 ) ∈ ( 𝐽 Cn 𝐽 ) )
41 1 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
42 41 a1i ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
43 35 39 40 42 cnmpt12f ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
44 34 43 eqeltrd ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
45 44 ex ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
46 4 7 10 13 21 45 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( 𝐽 Cn 𝐽 ) )