gg-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	gg-expcn.j	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	gg-expcn	$⊢ N \in ℕ_{0} \to (x \in ℂ ⟼ x^{N}) \in (J Cn J)$

Proof

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

Metamath Proof Explorer

Theorem gg-expcn

Proof