Metamath Proof Explorer

Theorem resqrtcn

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

Ref Expression
Assertion resqrtcn ⊢ √ ↾ 0 +∞ : 0 +∞ ⟶cn ℝ

Proof

Step Hyp Ref Expression
1 sqrtf ⊢ √ : ℂ ⟶ ℂ
2 1 a1i ⊢ ⊤ → √ : ℂ ⟶ ℂ
3 2 feqmptd ⊢ ⊤ → √ = x ∈ ℂ ⟼ x
4 3 reseq1d ⊢ ⊤ → √ ↾ 0 +∞ = x ∈ ℂ ⟼ x ↾ 0 +∞
5 elrege0 ⊢ x ∈ 0 +∞ ↔ x ∈ ℝ ∧ 0 ≤ x
6 5 simplbi ⊢ x ∈ 0 +∞ → x ∈ ℝ
7 6 recnd ⊢ x ∈ 0 +∞ → x ∈ ℂ
8 7 ssriv ⊢ 0 +∞ ⊆ ℂ
9 resmpt ⊢ 0 +∞ ⊆ ℂ → x ∈ ℂ ⟼ x ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x
10 8 9 mp1i ⊢ ⊤ → x ∈ ℂ ⟼ x ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x
11 4 10 eqtrd ⊢ ⊤ → √ ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x
12 11 mptru ⊢ √ ↾ 0 +∞ = x ∈ 0 +∞ ⟼ x
13 eqid ⊢ x ∈ 0 +∞ ⟼ x = x ∈ 0 +∞ ⟼ x
14 resqrtcl ⊢ x ∈ ℝ ∧ 0 ≤ x → x ∈ ℝ
15 5 14 sylbi ⊢ x ∈ 0 +∞ → x ∈ ℝ
16 13 15 fmpti ⊢ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶ ℝ
17 ax-resscn ⊢ ℝ ⊆ ℂ
18 cxpsqrt ⊢ x ∈ ℂ → x 1 2 = x
19 7 18 syl ⊢ x ∈ 0 +∞ → x 1 2 = x
20 19 mpteq2ia ⊢ x ∈ 0 +∞ ⟼ x 1 2 = x ∈ 0 +∞ ⟼ x
21 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
22 21 cnfldtopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
23 22 a1i ⊢ ⊤ → TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ
24 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ 0 +∞ ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
25 23 8 24 sylancl ⊢ ⊤ → TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ ∈ TopOn ⁡ 0 +∞
26 25 cnmptid ⊢ ⊤ → x ∈ 0 +∞ ⟼ x ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞
27 cnvimass ⊢ ℜ -1 ℝ + ⊆ dom ⁡ ℜ
28 ref ⊢ ℜ : ℂ ⟶ ℝ
29 28 fdmi ⊢ dom ⁡ ℜ = ℂ
30 27 29 sseqtri ⊢ ℜ -1 ℝ + ⊆ ℂ
31 resttopon ⊢ TopOpen ⁡ ℂ fld ∈ TopOn ⁡ ℂ ∧ ℜ -1 ℝ + ⊆ ℂ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ + ∈ TopOn ⁡ ℜ -1 ℝ +
32 23 30 31 sylancl ⊢ ⊤ → TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ + ∈ TopOn ⁡ ℜ -1 ℝ +
33 halfcn ⊢ 1 2 ∈ ℂ
34 1rp ⊢ 1 ∈ ℝ +
35 rphalfcl ⊢ 1 ∈ ℝ + → 1 2 ∈ ℝ +
36 34 35 ax-mp ⊢ 1 2 ∈ ℝ +
37 rpre ⊢ 1 2 ∈ ℝ + → 1 2 ∈ ℝ
38 rere ⊢ 1 2 ∈ ℝ → ℜ ⁡ 1 2 = 1 2
39 36 37 38 mp2b ⊢ ℜ ⁡ 1 2 = 1 2
40 39 36 eqeltri ⊢ ℜ ⁡ 1 2 ∈ ℝ +
41 ffn ⊢ ℜ : ℂ ⟶ ℝ → ℜ Fn ℂ
42 elpreima ⊢ ℜ Fn ℂ → 1 2 ∈ ℜ -1 ℝ + ↔ 1 2 ∈ ℂ ∧ ℜ ⁡ 1 2 ∈ ℝ +
43 28 41 42 mp2b ⊢ 1 2 ∈ ℜ -1 ℝ + ↔ 1 2 ∈ ℂ ∧ ℜ ⁡ 1 2 ∈ ℝ +
44 33 40 43 mpbir2an ⊢ 1 2 ∈ ℜ -1 ℝ +
45 44 a1i ⊢ ⊤ → 1 2 ∈ ℜ -1 ℝ +
46 25 32 45 cnmptc ⊢ ⊤ → x ∈ 0 +∞ ⟼ 1 2 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ Cn TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ +
47 eqid ⊢ ℜ -1 ℝ + = ℜ -1 ℝ +
48 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ = TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞
49 eqid ⊢ TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ + = TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ +
50 47 21 48 49 cxpcn3 ⊢ y ∈ 0 +∞ , z ∈ ℜ -1 ℝ + ⟼ y z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ × t TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ + Cn TopOpen ⁡ ℂ fld
51 50 a1i ⊢ ⊤ → y ∈ 0 +∞ , z ∈ ℜ -1 ℝ + ⟼ y z ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ × t TopOpen ⁡ ℂ fld ↾ 𝑡 ℜ -1 ℝ + Cn TopOpen ⁡ ℂ fld
52 oveq12 ⊢ y = x ∧ z = 1 2 → y z = x 1 2
53 25 26 46 25 32 51 52 cnmpt12 ⊢ ⊤ → x ∈ 0 +∞ ⟼ x 1 2 ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ Cn TopOpen ⁡ ℂ fld
54 ssid ⊢ ℂ ⊆ ℂ
55 22 toponrestid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld ↾ 𝑡 ℂ
56 21 48 55 cncfcn ⊢ 0 +∞ ⊆ ℂ ∧ ℂ ⊆ ℂ → 0 +∞ ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ Cn TopOpen ⁡ ℂ fld
57 8 54 56 mp2an ⊢ 0 +∞ ⟶cn ℂ = TopOpen ⁡ ℂ fld ↾ 𝑡 0 +∞ Cn TopOpen ⁡ ℂ fld
58 53 57 eleqtrrdi ⊢ ⊤ → x ∈ 0 +∞ ⟼ x 1 2 : 0 +∞ ⟶cn ℂ
59 20 58 eqeltrrid ⊢ ⊤ → x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℂ
60 59 mptru ⊢ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℂ
61 cncffvrn ⊢ ℝ ⊆ ℂ ∧ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℂ → x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℝ ↔ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶ ℝ
62 17 60 61 mp2an ⊢ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℝ ↔ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶ ℝ
63 16 62 mpbir ⊢ x ∈ 0 +∞ ⟼ x : 0 +∞ ⟶cn ℝ
64 12 63 eqeltri ⊢ √ ↾ 0 +∞ : 0 +∞ ⟶cn ℝ