Metamath Proof Explorer

Theorem sqrtcn

Description: Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypothesis sqrcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion sqrtcn ( √ ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )

Proof

Step Hyp Ref Expression
1 sqrcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 sqrtf ⊢ √ : ℂ ⟶ ℂ
3 2 a1i ⊢ ( ⊤ → √ : ℂ ⟶ ℂ )
4 3 feqmptd ⊢ ( ⊤ → √ = ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) )
5 4 reseq1d ⊢ ( ⊤ → ( √ ↾ 𝐷 ) = ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ 𝐷 ) )
6 difss ⊢ ( ℂ ∖ ( -∞ (,] 0 ) ) ⊆ ℂ
7 1 6 eqsstri ⊢ 𝐷 ⊆ ℂ
8 resmpt ⊢ ( 𝐷 ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) )
9 7 8 mp1i ⊢ ( ⊤ → ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) )
10 7 sseli ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
11 10 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ℂ )
12 cxpsqrt ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
13 11 12 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
14 13 eqcomd ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐷 ) → ( √ ‘ 𝑥 ) = ( 𝑥 ↑𝑐 ( 1 / 2 ) ) )
15 14 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( √ ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) )
16 5 9 15 3eqtrd ⊢ ( ⊤ → ( √ ↾ 𝐷 ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) )
17 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
18 17 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
19 18 a1i ⊢ ( ⊤ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
20 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝐷 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
21 19 7 20 sylancl ⊢ ( ⊤ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ∈ ( TopOn ‘ 𝐷 ) )
22 21 cnmptid ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ) )
23 ax-1cn ⊢ 1 ∈ ℂ
24 halfcl ⊢ ( 1 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
25 23 24 mp1i ⊢ ( ⊤ → ( 1 / 2 ) ∈ ℂ )
26 21 19 25 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( 1 / 2 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
27 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 )
28 1 17 27 cxpcn ⊢ ( 𝑦 ∈ 𝐷 , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
29 28 a1i ⊢ ( ⊤ → ( 𝑦 ∈ 𝐷 , 𝑧 ∈ ℂ ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
30 oveq12 ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = ( 1 / 2 ) ) → ( 𝑦 ↑𝑐 𝑧 ) = ( 𝑥 ↑𝑐 ( 1 / 2 ) ) )
31 21 22 26 21 19 29 30 cnmpt12 ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
32 ssid ⊢ ℂ ⊆ ℂ
33 18 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
34 17 27 33 cncfcn ⊢ ( ( 𝐷 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) ) )
35 7 32 34 mp2an ⊢ ( 𝐷 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝐷 ) Cn ( TopOpen ‘ ℂfld ) )
36 31 35 eleqtrrdi ⊢ ( ⊤ → ( 𝑥 ∈ 𝐷 ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ∈ ( 𝐷 –cn→ ℂ ) )
37 16 36 eqeltrd ⊢ ( ⊤ → ( √ ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ ) )
38 37 mptru ⊢ ( √ ↾ 𝐷 ) ∈ ( 𝐷 –cn→ ℂ )