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 ⟼ x A : D ⟶cn ℂ

Proof

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