Theorem 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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	cxpcn2.k	⊢ 𝐾 = ( 𝐽 ↾t ℝ+ )
Assertion	cxpcn2	⊢ ( 𝑥 ∈ ℝ+ , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		cxpcn2.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cxpcn2.k	⊢ 𝐾 = ( 𝐽 ↾t ℝ+ )
3	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
4		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
5		ax-1	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) )
6		eqid	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
7	6	ellogdm	⊢ ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
8	4 5 7	sylanbrc	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
9	8	ssriv	⊢ ℝ+ ⊆ ( ℂ ∖ ( -∞ (,] 0 ) )
10		cnex	⊢ ℂ ∈ V
11	10	difexi	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ V
12		restabs	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ℝ+ ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ∈ V ) → ( ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ ) )
13	3 9 11 12	mp3an	⊢ ( ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾t ℝ+ ) = ( 𝐽 ↾t ℝ+ )
14	2 13	eqtr4i	⊢ 𝐾 = ( ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ↾t ℝ+ )
15	3	a1i	⊢ ( ⊤ → 𝐽 ∈ ( TopOn ‘ ℂ ) )
16		difss	⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
17		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ) → ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
18	15 16 17	sylancl	⊢ ( ⊤ → ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
19	9	a1i	⊢ ( ⊤ → ℝ+ ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
20	3	toponrestid	⊢ 𝐽 = ( 𝐽 ↾t ℂ )
21		ssidd	⊢ ( ⊤ → ℂ ⊆ ℂ )
22		eqid	⊢ ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) )
23	6 1 22	cxpcn	⊢ ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t 𝐽 ) Cn 𝐽 )
24	23	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( ( 𝐽 ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t 𝐽 ) Cn 𝐽 ) )
25	14 18 19 20 15 21 24	cnmpt2res	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )
26	25	mptru	⊢ ( 𝑥 ∈ ℝ+ , 𝑦 ∈ ℂ ↦ ( 𝑥 ↑𝑐 𝑦 ) ) ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 )