Theorem rpsqrtcn

Description: Continuity of the real positive square root function. (Contributed by Thierry Arnoux, 20-Dec-2021)

	Ref	Expression
Assertion	rpsqrtcn	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}{ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3	1 2	sstri	$$⊢{ℝ}^{+}\subseteq ℂ$$
4		sqrtf	$$⊢\surd :ℂ⟶ℂ$$
5		fdm	$$⊢\surd :ℂ⟶ℂ\to \mathrm{dom}\surd =ℂ$$
6	4 5	ax-mp	$$⊢\mathrm{dom}\surd =ℂ$$
7	3 6	sseqtrri	$$⊢{ℝ}^{+}\subseteq \mathrm{dom}\surd$$
8	7	sseli	$$⊢x\in {ℝ}^{+}\to x\in \mathrm{dom}\surd$$
9		rpsqrtcl	$$⊢x\in {ℝ}^{+}\to \sqrt{x}\in {ℝ}^{+}$$
10	8 9	jca	$$⊢x\in {ℝ}^{+}\to \left(x\in \mathrm{dom}\surd \wedge \sqrt{x}\in {ℝ}^{+}\right)$$
11	10	rgen	$$⊢\forall x\in {ℝ}^{+}\left(x\in \mathrm{dom}\surd \wedge \sqrt{x}\in {ℝ}^{+}\right)$$
12		ffun	$$⊢\surd :ℂ⟶ℂ\to \mathrm{Fun}\surd$$
13	4 12	ax-mp	$$⊢\mathrm{Fun}\surd$$
14		ffvresb	$$⊢\mathrm{Fun}\surd \to \left(\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶{ℝ}^{+}\leftrightarrow \forall x\in {ℝ}^{+}\left(x\in \mathrm{dom}\surd \wedge \sqrt{x}\in {ℝ}^{+}\right)\right)$$
15	13 14	ax-mp	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶{ℝ}^{+}\leftrightarrow \forall x\in {ℝ}^{+}\left(x\in \mathrm{dom}\surd \wedge \sqrt{x}\in {ℝ}^{+}\right)$$
16	11 15	mpbir	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶{ℝ}^{+}$$
17		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
18		ioossico	$$⊢\left(0,\mathrm{+\infty }\right)\subseteq \left[0,\mathrm{+\infty }\right)$$
19	17 18	eqsstrri	$$⊢{ℝ}^{+}\subseteq \left[0,\mathrm{+\infty }\right)$$
20		resabs1	$$⊢{ℝ}^{+}\subseteq \left[0,\mathrm{+\infty }\right)\to {\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)\upharpoonright }_{{ℝ}^{+}}={\surd \upharpoonright }_{{ℝ}^{+}}$$
21	19 20	ax-mp	$$⊢{\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)\upharpoonright }_{{ℝ}^{+}}={\surd \upharpoonright }_{{ℝ}^{+}}$$
22		resqrtcn	$$⊢\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right):\left[0,\mathrm{+\infty }\right)\underset{cn}{⟶}ℝ$$
23		rescncf	$$⊢{ℝ}^{+}\subseteq \left[0,\mathrm{+\infty }\right)\to \left(\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right):\left[0,\mathrm{+\infty }\right)\underset{cn}{⟶}ℝ\to \left({\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ\right)$$
24	19 22 23	mp2	$$⊢\left({\left({\surd \upharpoonright }_{\left[0,\mathrm{+\infty }\right)}\right)\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ$$
25	21 24	eqeltrri	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ$$
26		cncffvrn	$$⊢\left({ℝ}^{+}\subseteq ℂ\wedge \left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}ℝ\right)\to \left(\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}{ℝ}^{+}\leftrightarrow \left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶{ℝ}^{+}\right)$$
27	3 25 26	mp2an	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}{ℝ}^{+}\leftrightarrow \left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶{ℝ}^{+}$$
28	16 27	mpbir	$$⊢\left({\surd \upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{cn}{⟶}{ℝ}^{+}$$