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 ⊢φ→A∈ℂ
cxpcncf1.d ⊢φ→D⊆ℂ∖−∞0
Assertion cxpcncf1 ⊢φ→x∈D⟼xA:D⟶cnℂ

Proof

Step Hyp Ref Expression
1 cxpcncf1.a ⊢φ→A∈ℂ
2 cxpcncf1.d ⊢φ→D⊆ℂ∖−∞0
3 resmpt ⊢D⊆ℂ∖−∞0→x∈ℂ∖−∞0⟼xA↾D=x∈D⟼xA
4 2 3 syl ⊢φ→x∈ℂ∖−∞0⟼xA↾D=x∈D⟼xA
5 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
6 5 cnfldtopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ
7 difss ⊢ℂ∖−∞0⊆ℂ
8 resttopon ⊢TopOpen⁡ℂfld∈TopOn⁡ℂ∧ℂ∖−∞0⊆ℂ→TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
9 6 7 8 mp2an ⊢TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
10 9 a1i ⊢φ→TopOpen⁡ℂfld↾𝑡ℂ∖−∞0∈TopOn⁡ℂ∖−∞0
11 10 cnmptid ⊢φ→x∈ℂ∖−∞0⟼x∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld↾𝑡ℂ∖−∞0
12 6 a1i ⊢φ→TopOpen⁡ℂfld∈TopOn⁡ℂ
13 10 12 1 cnmptc ⊢φ→x∈ℂ∖−∞0⟼A∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld
14 eqid ⊢ℂ∖−∞0=ℂ∖−∞0
15 eqid ⊢TopOpen⁡ℂfld↾𝑡ℂ∖−∞0=TopOpen⁡ℂfld↾𝑡ℂ∖−∞0
16 14 5 15 cxpcn ⊢y∈ℂ∖−∞0,z∈ℂ⟼yz∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
17 16 a1i ⊢φ→y∈ℂ∖−∞0,z∈ℂ⟼yz∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0×tTopOpen⁡ℂfldCnTopOpen⁡ℂfld
18 oveq12 ⊢y=x∧z=A→yz=xA
19 10 11 13 10 12 17 18 cnmpt12 ⊢φ→x∈ℂ∖−∞0⟼xA∈TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld
20 ssid ⊢ℂ⊆ℂ
21 6 toponrestid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld↾𝑡ℂ
22 5 15 21 cncfcn ⊢ℂ∖−∞0⊆ℂ∧ℂ⊆ℂ→ℂ∖−∞0⟶cnℂ=TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld
23 7 20 22 mp2an ⊢ℂ∖−∞0⟶cnℂ=TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld
24 23 eqcomi ⊢TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld=ℂ∖−∞0⟶cnℂ
25 24 a1i ⊢φ→TopOpen⁡ℂfld↾𝑡ℂ∖−∞0CnTopOpen⁡ℂfld=ℂ∖−∞0⟶cnℂ
26 19 25 eleqtrd ⊢φ→x∈ℂ∖−∞0⟼xA:ℂ∖−∞0⟶cnℂ
27 rescncf ⊢D⊆ℂ∖−∞0→x∈ℂ∖−∞0⟼xA:ℂ∖−∞0⟶cnℂ→x∈ℂ∖−∞0⟼xA↾D:D⟶cnℂ
28 27 imp ⊢D⊆ℂ∖−∞0∧x∈ℂ∖−∞0⟼xA:ℂ∖−∞0⟶cnℂ→x∈ℂ∖−∞0⟼xA↾D:D⟶cnℂ
29 2 26 28 syl2anc ⊢φ→x∈ℂ∖−∞0⟼xA↾D:D⟶cnℂ
30 4 29 eqeltrrd ⊢φ→x∈D⟼xA:D⟶cnℂ