Metamath Proof Explorer

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 ⊢ J = TopOpen ⁡ ℂ fld
cxpcn2.k ⊢ K = J ↾ 𝑡 ℝ +
Assertion cxpcn2 ⊢ x ∈ ℝ + , y ∈ ℂ ⟼ x y ∈ K × t J Cn J

Proof

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