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 \in ℕ_{0} \to (x \in ℂ ⟼ x^{N}) \in (J Cn J)$

Proof

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

Metamath Proof Explorer

Theorem expcn

Proof