This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐽 )