cxpcn2

Description: Continuity of the complex power function, when the base is real. (Contributed by Mario Carneiro, 1-May-2016)

	Ref	Expression
Hypotheses	cxpcn2.j	$⊢ J = TopOpen (ℂ_{fld})$
	cxpcn2.k	$⊢ K = J ↾_{𝑡} ℝ^{+}$
Assertion	cxpcn2	$⊢ (x \in ℝ^{+}, y \in ℂ ⟼ x^{y}) \in ((K \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		cxpcn2.j	$⊢ J = TopOpen (ℂ_{fld})$
2		cxpcn2.k	$⊢ K = J ↾_{𝑡} ℝ^{+}$
3	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
4		rpcn	$⊢ x \in ℝ^{+} \to x \in ℂ$
5		ax-1	$⊢ x \in ℝ^{+} \to (x \in ℝ \to x \in ℝ^{+})$
6		eqid	$⊢ ℂ ∖ (−∞, 0] = ℂ ∖ (−∞, 0]$
7	6	ellogdm	$⊢ x \in (ℂ ∖ (−∞, 0]) \leftrightarrow (x \in ℂ \land (x \in ℝ \to x \in ℝ^{+}))$
8	4 5 7	sylanbrc	$⊢ x \in ℝ^{+} \to x \in (ℂ ∖ (−∞, 0])$
9	8	ssriv	$⊢ ℝ^{+} \subseteq ℂ ∖ (−∞, 0]$
10		cnex	$⊢ ℂ \in V$
11	10	difexi	$⊢ ℂ ∖ (−∞, 0] \in V$
12		restabs	$⊢ (J \in TopOn (ℂ) \land ℝ^{+} \subseteq ℂ ∖ (−∞, 0] \land ℂ ∖ (−∞, 0] \in V) \to (J ↾_{𝑡} (ℂ ∖ (−∞, 0])) ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
13	3 9 11 12	mp3an	$⊢ (J ↾_{𝑡} (ℂ ∖ (−∞, 0])) ↾_{𝑡} ℝ^{+} = J ↾_{𝑡} ℝ^{+}$
14	2 13	eqtr4i	$⊢ K = (J ↾_{𝑡} (ℂ ∖ (−∞, 0])) ↾_{𝑡} ℝ^{+}$
15	3	a1i	$⊢ ⊤ \to J \in TopOn (ℂ)$
16		difss	$⊢ ℂ ∖ (−∞, 0] \subseteq ℂ$
17		resttopon	$⊢ (J \in TopOn (ℂ) \land ℂ ∖ (−∞, 0] \subseteq ℂ) \to J ↾_{𝑡} (ℂ ∖ (−∞, 0]) \in TopOn (ℂ ∖ (−∞, 0])$
18	15 16 17	sylancl	$⊢ ⊤ \to J ↾_{𝑡} (ℂ ∖ (−∞, 0]) \in TopOn (ℂ ∖ (−∞, 0])$
19	9	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℂ ∖ (−∞, 0]$
20	3	toponrestid	$⊢ J = J ↾_{𝑡} ℂ$
21		ssidd	$⊢ ⊤ \to ℂ \subseteq ℂ$
22		eqid	$⊢ J ↾_{𝑡} (ℂ ∖ (−∞, 0]) = J ↾_{𝑡} (ℂ ∖ (−∞, 0])$
23	6 1 22	cxpcn	$⊢ (x \in (ℂ ∖ (−∞, 0]), y \in ℂ ⟼ x^{y}) \in (((J ↾_{𝑡} (ℂ ∖ (−∞, 0])) \times_{t} J) Cn J)$
24	23	a1i	$⊢ ⊤ \to (x \in (ℂ ∖ (−∞, 0]), y \in ℂ ⟼ x^{y}) \in (((J ↾_{𝑡} (ℂ ∖ (−∞, 0])) \times_{t} J) Cn J)$
25	14 18 19 20 15 21 24	cnmpt2res	$⊢ ⊤ \to (x \in ℝ^{+}, y \in ℂ ⟼ x^{y}) \in ((K \times_{t} J) Cn J)$
26	25	mptru	$⊢ (x \in ℝ^{+}, y \in ℂ ⟼ x^{y}) \in ((K \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem cxpcn2

Proof