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 ⊢ ( ⊤ → √ = ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) )
4 3 reseq1d ⊢ ( ⊤ → ( √ ↾ ( 0 [,) +∞ ) ) = ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) ) )
5 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
6 5 simplbi ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℝ )
7 6 recnd ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → 𝑥 ∈ ℂ )
8 7 ssriv ⊢ ( 0 [,) +∞ ) ⊆ ℂ
9 resmpt ⊢ ( ( 0 [,) +∞ ) ⊆ ℂ → ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) )
10 8 9 mp1i ⊢ ( ⊤ → ( ( 𝑥 ∈ ℂ ↦ ( √ ‘ 𝑥 ) ) ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) )
11 4 10 eqtrd ⊢ ( ⊤ → ( √ ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) )
12 11 mptru ⊢ ( √ ↾ ( 0 [,) +∞ ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) )
13 eqid ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) )
14 resqrtcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( √ ‘ 𝑥 ) ∈ ℝ )
15 5 14 sylbi ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( √ ‘ 𝑥 ) ∈ ℝ )
16 13 15 fmpti ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) : ( 0 [,) +∞ ) ⟶ ℝ
17 ax-resscn ⊢ ℝ ⊆ ℂ
18 cxpsqrt ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
19 7 18 syl ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) → ( 𝑥 ↑𝑐 ( 1 / 2 ) ) = ( √ ‘ 𝑥 ) )
20 19 mpteq2ia ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) = ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) )
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 ) ↾t ( 0 [,) +∞ ) ) ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) )
25 23 8 24 sylancl ⊢ ( ⊤ → ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ∈ ( TopOn ‘ ( 0 [,) +∞ ) ) )
26 25 cnmptid ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ) )
27 cnvimass ⊢ ( ◡ ℜ “ ℝ+ ) ⊆ dom ℜ
28 ref ⊢ ℜ : ℂ ⟶ ℝ
29 28 fdmi ⊢ dom ℜ = ℂ
30 27 29 sseqtri ⊢ ( ◡ ℜ “ ℝ+ ) ⊆ ℂ
31 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ◡ ℜ “ ℝ+ ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) ∈ ( TopOn ‘ ( ◡ ℜ “ ℝ+ ) ) )
32 23 30 31 sylancl ⊢ ( ⊤ → ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) ∈ ( TopOn ‘ ( ◡ ℜ “ ℝ+ ) ) )
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 / 2 ) ∈ ℂ ∧ ( ℜ ‘ ( 1 / 2 ) ) ∈ ℝ+ ) ) )
43 28 41 42 mp2b ⊢ ( ( 1 / 2 ) ∈ ( ◡ ℜ “ ℝ+ ) ↔ ( ( 1 / 2 ) ∈ ℂ ∧ ( ℜ ‘ ( 1 / 2 ) ) ∈ ℝ+ ) )
44 33 40 43 mpbir2an ⊢ ( 1 / 2 ) ∈ ( ◡ ℜ “ ℝ+ )
45 44 a1i ⊢ ( ⊤ → ( 1 / 2 ) ∈ ( ◡ ℜ “ ℝ+ ) )
46 25 32 45 cnmptc ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( 1 / 2 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) ) )
47 eqid ⊢ ( ◡ ℜ “ ℝ+ ) = ( ◡ ℜ “ ℝ+ )
48 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) )
49 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) )
50 47 21 48 49 cxpcn3 ⊢ ( 𝑦 ∈ ( 0 [,) +∞ ) , 𝑧 ∈ ( ◡ ℜ “ ℝ+ ) ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) ) Cn ( TopOpen ‘ ℂfld ) )
51 50 a1i ⊢ ( ⊤ → ( 𝑦 ∈ ( 0 [,) +∞ ) , 𝑧 ∈ ( ◡ ℜ “ ℝ+ ) ↦ ( 𝑦 ↑𝑐 𝑧 ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ◡ ℜ “ ℝ+ ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
52 oveq12 ⊢ ( ( 𝑦 = 𝑥 ∧ 𝑧 = ( 1 / 2 ) ) → ( 𝑦 ↑𝑐 𝑧 ) = ( 𝑥 ↑𝑐 ( 1 / 2 ) ) )
53 25 26 46 25 32 51 52 cnmpt12 ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( TopOpen ‘ ℂfld ) ) )
54 ssid ⊢ ℂ ⊆ ℂ
55 22 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
56 21 48 55 cncfcn ⊢ ( ( ( 0 [,) +∞ ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 0 [,) +∞ ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( TopOpen ‘ ℂfld ) ) )
57 8 54 56 mp2an ⊢ ( ( 0 [,) +∞ ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 0 [,) +∞ ) ) Cn ( TopOpen ‘ ℂfld ) )
58 53 57 eleqtrrdi ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( 𝑥 ↑𝑐 ( 1 / 2 ) ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℂ ) )
59 20 58 eqeltrrid ⊢ ( ⊤ → ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℂ ) )
60 59 mptru ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℂ )
61 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℂ ) ) → ( ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) : ( 0 [,) +∞ ) ⟶ ℝ ) )
62 17 60 61 mp2an ⊢ ( ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ ) ↔ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) : ( 0 [,) +∞ ) ⟶ ℝ )
63 16 62 mpbir ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↦ ( √ ‘ 𝑥 ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ )
64 12 63 eqeltri ⊢ ( √ ↾ ( 0 [,) +∞ ) ) ∈ ( ( 0 [,) +∞ ) –cn→ ℝ )