Theorem cxpcn

Description: Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	cxpcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
	cxpcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	cxpcn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝐷 )
Assertion	cxpcn	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		cxpcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2		cxpcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
3		cxpcn.k	⊢ 𝐾 = ( 𝐽 ↾t 𝐷 )
4	1	ellogdm	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
5	4	simplbi	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
6	5	adantr	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑥 ∈ ℂ )
7	1	logdmn0	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
8	7	adantr	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑥 ≠ 0 )
9		simpr	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
10	6 8 9	cxpefd	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ↑𝑐 𝑦 ) = ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
11	10	mpoeq3ia	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) )
12	2	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
13	12	a1i	⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
14	5	ssriv	⊢ 𝐷 ⊆ ℂ
15		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
16	13 14 15	sylancl	⊢ ( ⊤ → ( 𝐽 ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
17	3 16	eqeltrid	⊢ ( ⊤ → 𝐾 ∈ ( TopOn ‘ 𝐷 ) )
18	17 13	cnmpt2nd	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ 𝑦 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
19		fvres	⊢ ( 𝑥 ∈ 𝐷 → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
20	19	adantr	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ ℂ ) → ( ( log ↾ 𝐷 ) ‘ 𝑥 ) = ( log ‘ 𝑥 ) )
21	20	mpoeq3ia	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( log ‘ 𝑥 ) )
22	17 13	cnmpt1st	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ 𝑥 ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐾 ) )
23	1	logcn	⊢ ( log ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )
24		ssid	⊢ ℂ ⊆ ℂ
25	12	toponrestid	⊢ 𝐽 = ( 𝐽 ↾t ℂ )
26	2 3 25	cncfcn	⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℂ ) = ( 𝐾 Cn 𝐽 ) )
27	14 24 26	mp2an	⊢ ( 𝐷 –cn→ ℂ ) = ( 𝐾 Cn 𝐽 )
28	23 27	eleqtri	⊢ ( log ↾ 𝐷 ) ∈ ( 𝐾 Cn 𝐽 )
29	28	a1i	⊢ ( ⊤ → ( log ↾ 𝐷 ) ∈ ( 𝐾 Cn 𝐽 ) )
30	17 13 22 29	cnmpt21f	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( ( log ↾ 𝐷 ) ‘ 𝑥 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
31	21 30	eqeltrrid	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( log ‘ 𝑥 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
32	2	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
33	32	a1i	⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
34		oveq12	⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = ( log ‘ 𝑥 ) ) → ( 𝑢 · 𝑣 ) = ( 𝑦 · ( log ‘ 𝑥 ) ) )
35	17 13 18 31 13 13 33 34	cnmpt22	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
36		efcn	⊢ exp ∈ ( ℂ –cn→ ℂ )
37	2	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( 𝐽 Cn 𝐽 )
38	36 37	eleqtri	⊢ exp ∈ ( 𝐽 Cn 𝐽 )
39	38	a1i	⊢ ( ⊤ → exp ∈ ( 𝐽 Cn 𝐽 ) )
40	17 13 35 39	cnmpt21f	⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
41	40	mptru	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( exp ‘ ( 𝑦 · ( log ‘ 𝑥 ) ) ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )
42	11 41	eqeltri	⊢ ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )