resqrtcn

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

		Ref	Expression
	Assertion	resqrtcn	$⊢ ({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
2	1	a1i	$⊢ ⊤ \to \sqrt : ℂ ⟶ ℂ$
3	2	feqmptd	$⊢ ⊤ \to \sqrt = (x \in ℂ ⟼ \sqrt{x})$
4	3	reseq1d	$⊢ ⊤ \to {\sqrt ↾}_{[0, +∞)} = {(x \in ℂ ⟼ \sqrt{x}) ↾}_{[0, +∞)}$
5		elrege0	$⊢ x \in [0, +∞) \leftrightarrow (x \in ℝ \land 0 \leq x)$
6	5	simplbi	$⊢ x \in [0, +∞) \to x \in ℝ$
7	6	recnd	$⊢ x \in [0, +∞) \to x \in ℂ$
8	7	ssriv	$⊢ [0, +∞) \subseteq ℂ$
9		resmpt	$⊢ [0, +∞) \subseteq ℂ \to {(x \in ℂ ⟼ \sqrt{x}) ↾}_{[0, +∞)} = (x \in [0, +∞) ⟼ \sqrt{x})$
10	8 9	mp1i	$⊢ ⊤ \to {(x \in ℂ ⟼ \sqrt{x}) ↾}_{[0, +∞)} = (x \in [0, +∞) ⟼ \sqrt{x})$
11	4 10	eqtrd	$⊢ ⊤ \to {\sqrt ↾}_{[0, +∞)} = (x \in [0, +∞) ⟼ \sqrt{x})$
12	11	mptru	$⊢ {\sqrt ↾}_{[0, +∞)} = (x \in [0, +∞) ⟼ \sqrt{x})$
13		eqid	$⊢ (x \in [0, +∞) ⟼ \sqrt{x}) = (x \in [0, +∞) ⟼ \sqrt{x})$
14		resqrtcl	$⊢ (x \in ℝ \land 0 \leq x) \to \sqrt{x} \in ℝ$
15	5 14	sylbi	$⊢ x \in [0, +∞) \to \sqrt{x} \in ℝ$
16	13 15	fmpti	$⊢ (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) ⟶ ℝ$
17		ax-resscn	$⊢ ℝ \subseteq ℂ$
18		cxpsqrt	$⊢ x \in ℂ \to x^{\frac{1}{2}} = \sqrt{x}$
19	7 18	syl	$⊢ x \in [0, +∞) \to x^{\frac{1}{2}} = \sqrt{x}$
20	19	mpteq2ia	$⊢ (x \in [0, +∞) ⟼ x^{\frac{1}{2}}) = (x \in [0, +∞) ⟼ \sqrt{x})$
21		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
22	21	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
23	22	a1i	$⊢ ⊤ \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
24		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land [0, +∞) \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) \in TopOn ([0, +∞))$
25	23 8 24	sylancl	$⊢ ⊤ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) \in TopOn ([0, +∞))$
26	25	cnmptid	$⊢ ⊤ \to (x \in [0, +∞) ⟼ x) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)))$
27		cnvimass	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq dom ℜ$
28		ref	$⊢ ℜ : ℂ ⟶ ℝ$
29	28	fdmi	$⊢ dom ℜ = ℂ$
30	27 29	sseqtri	$⊢ ℜ^{-1} [ℝ^{+}] \subseteq ℂ$
31		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land ℜ^{-1} [ℝ^{+}] \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℜ^{-1} [ℝ^{+}] \in TopOn (ℜ^{-1} [ℝ^{+}])$
32	23 30 31	sylancl	$⊢ ⊤ \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℜ^{-1} [ℝ^{+}] \in TopOn (ℜ^{-1} [ℝ^{+}])$
33		halfcn	$⊢ \frac{1}{2} \in ℂ$
34		1rp	$⊢ 1 \in ℝ^{+}$
35		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
36	34 35	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
37		rpre	$⊢ \frac{1}{2} \in ℝ^{+} \to \frac{1}{2} \in ℝ$
38		rere	$⊢ \frac{1}{2} \in ℝ \to ℜ (\frac{1}{2}) = \frac{1}{2}$
39	36 37 38	mp2b	$⊢ ℜ (\frac{1}{2}) = \frac{1}{2}$
40	39 36	eqeltri	$⊢ ℜ (\frac{1}{2}) \in ℝ^{+}$
41		ffn	$⊢ ℜ : ℂ ⟶ ℝ \to ℜ Fn ℂ$
42		elpreima	$⊢ ℜ Fn ℂ \to (\frac{1}{2} \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (\frac{1}{2} \in ℂ \land ℜ (\frac{1}{2}) \in ℝ^{+}))$
43	28 41 42	mp2b	$⊢ \frac{1}{2} \in ℜ^{-1} [ℝ^{+}] \leftrightarrow (\frac{1}{2} \in ℂ \land ℜ (\frac{1}{2}) \in ℝ^{+})$
44	33 40 43	mpbir2an	$⊢ \frac{1}{2} \in ℜ^{-1} [ℝ^{+}]$
45	44	a1i	$⊢ ⊤ \to \frac{1}{2} \in ℜ^{-1} [ℝ^{+}]$
46	25 32 45	cnmptc	$⊢ ⊤ \to (x \in [0, +∞) ⟼ \frac{1}{2}) \in ((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 \in [0, +∞), z \in ℜ^{-1} [ℝ^{+}] ⟼ y^{z}) \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) \times_{t} (TopOpen (ℂ_{fld}) ↾_{𝑡} ℜ^{-1} [ℝ^{+}])) Cn TopOpen (ℂ_{fld}))$
51	50	a1i	$⊢ ⊤ \to (y \in [0, +∞), z \in ℜ^{-1} [ℝ^{+}] ⟼ y^{z}) \in (((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) \times_{t} (TopOpen (ℂ_{fld}) ↾_{𝑡} ℜ^{-1} [ℝ^{+}])) Cn TopOpen (ℂ_{fld}))$
52		oveq12	$⊢ (y = x \land z = \frac{1}{2}) \to y^{z} = x^{\frac{1}{2}}$
53	25 26 46 25 32 51 52	cnmpt12	$⊢ ⊤ \to (x \in [0, +∞) ⟼ x^{\frac{1}{2}}) \in ((TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn TopOpen (ℂ_{fld}))$
54		ssid	$⊢ ℂ \subseteq ℂ$
55	22	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
56	21 48 55	cncfcn	$⊢ ([0, +∞) \subseteq ℂ \land ℂ \subseteq ℂ) \to [0, +∞) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn TopOpen (ℂ_{fld})$
57	8 54 56	mp2an	$⊢ [0, +∞) \underset{cn}{⟶} ℂ = (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) Cn TopOpen (ℂ_{fld})$
58	53 57	eleqtrrdi	$⊢ ⊤ \to (x \in [0, +∞) ⟼ x^{\frac{1}{2}}) : [0, +∞) \underset{cn}{⟶} ℂ$
59	20 58	eqeltrrid	$⊢ ⊤ \to (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℂ$
60	59	mptru	$⊢ (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℂ$
61		cncfcdm	$⊢ (ℝ \subseteq ℂ \land (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℂ) \to ((x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℝ \leftrightarrow (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) ⟶ ℝ)$
62	17 60 61	mp2an	$⊢ (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℝ \leftrightarrow (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) ⟶ ℝ$
63	16 62	mpbir	$⊢ (x \in [0, +∞) ⟼ \sqrt{x}) : [0, +∞) \underset{cn}{⟶} ℝ$
64	12 63	eqeltri	$⊢ ({\sqrt ↾}_{[0, +∞)}) : [0, +∞) \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem resqrtcn

Proof