Metamath Proof Explorer

Theorem sqrtcn

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

Ref Expression
Hypothesis sqrcn.d ⊢ D = ℂ ∖ −∞ 0
Assertion sqrtcn ⊢ √ ↾ D : D ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 sqrcn.d ⊢ D = ℂ ∖ −∞ 0
2 sqrtf ⊢ √ : ℂ ⟶ ℂ
3 2 a1i ⊢ ⊤ → √ : ℂ ⟶ ℂ
4 3 feqmptd ⊢ ⊤ → √ = x ∈ ℂ ⟼ x
5 4 reseq1d ⊢ ⊤ → √ ↾ D = x ∈ ℂ ⟼ x ↾ D
6 difss ⊢ ℂ ∖ −∞ 0 ⊆ ℂ
7 1 6 eqsstri ⊢ D ⊆ ℂ
8 resmpt ⊢ D ⊆ ℂ → x ∈ ℂ ⟼ x ↾ D = x ∈ D ⟼ x
9 7 8 mp1i ⊢ ⊤ → x ∈ ℂ ⟼ x ↾ D = x ∈ D ⟼ x
10 7 sseli ⊢ x ∈ D → x ∈ ℂ
11 10 adantl ⊢ ⊤ ∧ x ∈ D → x ∈ ℂ
12 cxpsqrt ⊢ x ∈ ℂ → x 1 2 = x
13 11 12 syl ⊢ ⊤ ∧ x ∈ D → x 1 2 = x
14 13 eqcomd ⊢ ⊤ ∧ x ∈ D → x = x 1 2
15 14 mpteq2dva ⊢ ⊤ → x ∈ D ⟼ x = x ∈ D ⟼ x 1 2
16 5 9 15 3eqtrd ⊢ ⊤ → √ ↾ D = x ∈ D ⟼ x 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 ⁡ ℂ ∧ D ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 D ∈ TopOn ⁡ D
21 19 7 20 sylancl ⊢ ⊤ → TopOpen ⁡ ℂ fld ↾ 𝑡 D ∈ TopOn ⁡ D
22 21 cnmptid ⊢ ⊤ → x ∈ D ⟼ x ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 D Cn TopOpen ⁡ ℂ fld ↾ 𝑡 D
23 ax-1cn ⊢ 1 ∈ ℂ
24 halfcl ⊢ 1 ∈ ℂ → 1 2 ∈ ℂ
25 23 24 mp1i ⊢ ⊤ → 1 2 ∈ ℂ
26 21 19 25 cnmptc ⊢ ⊤ → x ∈ D ⟼ 1 2 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 D Cn TopOpen ⁡ ℂ fld
27 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 D = TopOpen ⁡ ℂ fld ↾ 𝑡 D
28 1 17 27 cxpcn ⊢ y ∈ D , z ∈ ℂ ⟼ y z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 D × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
29 28 a1i ⊢ ⊤ → y ∈ D , z ∈ ℂ ⟼ y z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 D × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
30 oveq12 ⊢ y = x ∧ z = 1 2 → y z = x 1 2
31 21 22 26 21 19 29 30 cnmpt12 ⊢ ⊤ → x ∈ D ⟼ x 1 2 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 D Cn TopOpen ⁡ ℂ fld
32 ssid ⊢ ℂ ⊆ ℂ
33 18 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
34 17 27 33 cncfcn ⊢ D ⊆ ℂ ∧ ℂ ⊆ ℂ → D ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 D Cn TopOpen ⁡ ℂ fld
35 7 32 34 mp2an ⊢ D ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 D Cn TopOpen ⁡ ℂ fld
36 31 35 eleqtrrdi ⊢ ⊤ → x ∈ D ⟼ x 1 2 : D ⟶cn ℂ
37 16 36 eqeltrd ⊢ ⊤ → √ ↾ D : D ⟶cn ℂ
38 37 mptru ⊢ √ ↾ D : D ⟶cn ℂ