gg-cxpcn

Description: Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016) Use mpomulcn instead of mulcn as direct dependency. (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	gg-cxpcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
	gg-cxpcn.j	$⊢ J = TopOpen (ℂ_{fld})$
	gg-cxpcn.k	$⊢ K = J ↾_{𝑡} D$
Assertion	gg-cxpcn	$⊢ (x \in D, y \in ℂ ⟼ x^{y}) \in ((K \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		gg-cxpcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		gg-cxpcn.j	$⊢ J = TopOpen (ℂ_{fld})$
3		gg-cxpcn.k	$⊢ K = J ↾_{𝑡} D$
4	1	ellogdm	$⊢ x \in D \leftrightarrow (x \in ℂ \land (x \in ℝ \to x \in ℝ^{+}))$
5	4	simplbi	$⊢ x \in D \to x \in ℂ$
6	5	adantr	$⊢ (x \in D \land y \in ℂ) \to x \in ℂ$
7	1	logdmn0	$⊢ x \in D \to x \neq 0$
8	7	adantr	$⊢ (x \in D \land y \in ℂ) \to x \neq 0$
9		simpr	$⊢ (x \in D \land y \in ℂ) \to y \in ℂ$
10	6 8 9	cxpefd	$⊢ (x \in D \land y \in ℂ) \to x^{y} = e^{y \log x}$
11	10	mpoeq3ia	$⊢ (x \in D, y \in ℂ ⟼ x^{y}) = (x \in D, y \in ℂ ⟼ e^{y \log x})$
12	2	cnfldtopon	$⊢ J \in TopOn (ℂ)$
13	12	a1i	$⊢ ⊤ \to J \in TopOn (ℂ)$
14	5	ssriv	$⊢ D \subseteq ℂ$
15		resttopon	$⊢ (J \in TopOn (ℂ) \land D \subseteq ℂ) \to J ↾_{𝑡} D \in TopOn (D)$
16	13 14 15	sylancl	$⊢ ⊤ \to J ↾_{𝑡} D \in TopOn (D)$
17	3 16	eqeltrid	$⊢ ⊤ \to K \in TopOn (D)$
18	17 13	cnmpt2nd	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ y) \in ((K \times_{t} J) Cn J)$
19		fvres	$⊢ x \in D \to ({log ↾}_{D}) (x) = \log x$
20	19	adantr	$⊢ (x \in D \land y \in ℂ) \to ({log ↾}_{D}) (x) = \log x$
21	20	mpoeq3ia	$⊢ (x \in D, y \in ℂ ⟼ ({log ↾}_{D}) (x)) = (x \in D, y \in ℂ ⟼ \log x)$
22	17 13	cnmpt1st	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ x) \in ((K \times_{t} J) Cn K)$
23	1	logcn	$⊢ ({log ↾}_{D}) : D \underset{cn}{⟶} ℂ$
24		ssid	$⊢ ℂ \subseteq ℂ$
25	12	toponrestid	$⊢ J = J ↾_{𝑡} ℂ$
26	2 3 25	cncfcn	$⊢ (D \subseteq ℂ \land ℂ \subseteq ℂ) \to D \underset{cn}{⟶} ℂ = K Cn J$
27	14 24 26	mp2an	$⊢ D \underset{cn}{⟶} ℂ = K Cn J$
28	23 27	eleqtri	$⊢ {log ↾}_{D} \in (K Cn J)$
29	28	a1i	$⊢ ⊤ \to {log ↾}_{D} \in (K Cn J)$
30	17 13 22 29	cnmpt21f	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ ({log ↾}_{D}) (x)) \in ((K \times_{t} J) Cn J)$
31	21 30	eqeltrrid	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ \log x) \in ((K \times_{t} J) Cn J)$
32	2	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
33	32	a1i	$⊢ ⊤ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
34		oveq12	$⊢ (u = y \land v = \log x) \to u v = y \log x$
35	17 13 18 31 13 13 33 34	cnmpt22	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ y \log x) \in ((K \times_{t} J) Cn J)$
36		efcn	$⊢ \exp : ℂ \underset{cn}{⟶} ℂ$
37	2	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = J Cn J$
38	36 37	eleqtri	$⊢ \exp \in (J Cn J)$
39	38	a1i	$⊢ ⊤ \to \exp \in (J Cn J)$
40	17 13 35 39	cnmpt21f	$⊢ ⊤ \to (x \in D, y \in ℂ ⟼ e^{y \log x}) \in ((K \times_{t} J) Cn J)$
41	40	mptru	$⊢ (x \in D, y \in ℂ ⟼ e^{y \log x}) \in ((K \times_{t} J) Cn J)$
42	11 41	eqeltri	$⊢ (x \in D, y \in ℂ ⟼ x^{y}) \in ((K \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem gg-cxpcn

Proof