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	⊢ 𝐽 = ( 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	24 25 26	syl2anr	⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑛 ∈ ℂ ) → ( 𝑛 ↑ ( 𝑘 + 1 ) ) = ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) )
28	27	mpteq2dva	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) ) )
29	23 28	eqtrid	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) = ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) ) )
30	16	a1i	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
31		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 ↑ 𝑘 ) = ( 𝑛 ↑ 𝑘 ) )
32	31	cbvmptv	⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) = ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ 𝑘 ) )
33		simpr	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
34	32 33	eqeltrrid	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( 𝑛 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
35	30	cnmptid	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ 𝑛 ) ∈ ( 𝐽 Cn 𝐽 ) )
36	1	mulcn	⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
37	36	a1i	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
38	30 34 35 37	cnmpt12f	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑛 ∈ ℂ ↦ ( ( 𝑛 ↑ 𝑘 ) · 𝑛 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
39	29 38	eqeltrd	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
40	39	ex	⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑘 ) ) ∈ ( 𝐽 Cn 𝐽 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ ( 𝑘 + 1 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
41	4 7 10 13 21 40	nn0ind	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ 𝑁 ) ) ∈ ( 𝐽 Cn 𝐽 ) )