Metamath Proof Explorer

Theorem cxpcncf1

Description: The power function on complex numbers, for fixed exponent A, is continuous. Similar to cxpcn . (Contributed by Thierry Arnoux, 20-Dec-2021)

Ref Expression
Hypotheses cxpcncf1.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
cxpcncf1.d ⊢ ( 𝜑 → 𝐷 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
Assertion cxpcncf1 ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( 𝐷 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 cxpcncf1.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 cxpcncf1.d ⊢ ( 𝜑 → 𝐷 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) )
3 resmpt ⊢ ( 𝐷 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) )
4 2 3 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) )
5 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
6 5 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
7 difss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
8 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
9 6 7 8 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) )
10 9 a1i ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
11 10 cnmptid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
12 6 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
13 10 12 1 cnmptc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
14 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
15 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) )
16 14 5 15 cxpcn ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
17 16 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
18 oveq12 ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = 𝐴 ) → ( 𝑦 ↑𝑐 𝑧 ) = ( 𝑥 ↑𝑐 𝐴 ) )
19 10 11 13 10 12 17 18 cnmpt12 ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
20 ssid ⊢ ℂ ⊆ ℂ
21 6 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
22 5 15 21 cncfcn ⊢ ( ( ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
23 7 20 22 mp2an ⊢ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) )
24 23 eqcomi ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ )
25 24 a1i ⊢ ( 𝜑 → ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) Cn ( TopOpen ‘ ℂfld ) ) = ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) )
26 19 25 eleqtrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) )
27 rescncf ⊢ ( 𝐷 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) ) )
28 27 imp ⊢ ( ( 𝐷 ⊆ ( ℂ ∖ ( -∞ (,] 0 ) ) ∧ ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( ( ℂ ∖ ( -∞ (,] 0 ) ) –cn→ ℂ ) ) → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) )
29 2 26 28 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) )
30 4 29 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 𝐴 ) ) ∈ ( 𝐷 –cn→ ℂ ) )