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

Metamath Proof Explorer

Theorem cxpcncf2

Description: The complex power function is continuous with respect to its second argument. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Assertion cxpcncf2 ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2 1 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
3 2 a1i ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
4 difss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
5 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
6 2 4 5 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) )
7 6 a1i ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) )
8 id ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
9 snidg ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → 𝐴 ∈ { 𝐴 } )
10 9 adantr ⊢ ( ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ∧ 𝑥 ∈ ℂ ) → 𝐴 ∈ { 𝐴 } )
11 10 fmpttd ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) : ℂ ⟶ { 𝐴 } )
12 cnconst ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ∈ ( TopOn ‘ ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) ∧ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ∧ ( 𝑥 ∈ ℂ ↦ 𝐴 ) : ℂ ⟶ { 𝐴 } ) ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
13 3 7 8 11 12 syl22anc ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ) )
14 3 cnmptid ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
15 eqid ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) = ( ℂ ∖ ( -∞ (,] 0 ) )
16 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) )
17 15 1 16 cxpcn ⊢ ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
18 17 a1i ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑦 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ ( -∞ (,] 0 ) ) ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
19 oveq12 ⊢ ( ( 𝑦 = 𝐴 ∧ 𝑧 = 𝑥 ) → ( 𝑦 ↑𝑐 𝑧 ) = ( 𝐴 ↑𝑐 𝑥 ) )
20 3 13 14 7 3 18 19 cnmpt12 ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
21 ssid ⊢ ℂ ⊆ ℂ
22 2 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
23 1 22 22 cncfcn ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
24 21 21 23 mp2an ⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
25 24 eqcomi ⊢ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) = ( ℂ –cn→ ℂ )
26 25 a1i ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) = ( ℂ –cn→ ℂ ) )
27 20 26 eleqtrd ⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ( 𝑥 ∈ ℂ ↦ ( 𝐴 ↑𝑐 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )