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	$⊢ 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		expcl	$⊢ (n \in ℂ \land k \in ℕ_{0}) \to n^{k} \in ℂ$
28		simpl	$⊢ (n \in ℂ \land k \in ℕ_{0}) \to n \in ℂ$
29		ovmpot	$⊢ (n^{k} \in ℂ \land n \in ℂ) \to n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n = n^{k} n$
30	27 28 29	syl2anc	$⊢ (n \in ℂ \land k \in ℕ_{0}) \to n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n = n^{k} n$
31	26 30	eqtr4d	$⊢ (n \in ℂ \land k \in ℕ_{0}) \to n^{k + 1} = n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n$
32	24 25 31	syl2anr	$⊢ ((k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \land n \in ℂ) \to n^{k + 1} = n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n$
33	32	mpteq2dva	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (n \in ℂ ⟼ n^{k + 1}) = (n \in ℂ ⟼ n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n)$
34	23 33	eqtrid	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (x \in ℂ ⟼ x^{k + 1}) = (n \in ℂ ⟼ n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n)$
35	16	a1i	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to J \in TopOn (ℂ)$
36		oveq1	$⊢ x = n \to x^{k} = n^{k}$
37	36	cbvmptv	$⊢ (x \in ℂ ⟼ x^{k}) = (n \in ℂ ⟼ n^{k})$
38		simpr	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (x \in ℂ ⟼ x^{k}) \in (J Cn J)$
39	37 38	eqeltrrid	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (n \in ℂ ⟼ n^{k}) \in (J Cn J)$
40	35	cnmptid	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (n \in ℂ ⟼ n) \in (J Cn J)$
41	1	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
42	41	a1i	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
43	35 39 40 42	cnmpt12f	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (n \in ℂ ⟼ n^{k} (u \in ℂ, v \in ℂ ⟼ u v) n) \in (J Cn J)$
44	34 43	eqeltrd	$⊢ (k \in ℕ_{0} \land (x \in ℂ ⟼ x^{k}) \in (J Cn J)) \to (x \in ℂ ⟼ x^{k + 1}) \in (J Cn J)$
45	44	ex	$⊢ k \in ℕ_{0} \to ((x \in ℂ ⟼ x^{k}) \in (J Cn J) \to (x \in ℂ ⟼ x^{k + 1}) \in (J Cn J))$
46	4 7 10 13 21 45	nn0ind	$⊢ N \in ℕ_{0} \to (x \in ℂ ⟼ x^{N}) \in (J Cn J)$

Metamath Proof Explorer

Theorem expcn

Proof