Theorem sqrtcn

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

	Ref	Expression
Hypothesis	sqrcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	sqrtcn	$$⊢\left({\surd \upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sqrcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		sqrtf	$$⊢\surd :ℂ⟶ℂ$$
3	2	a1i	$$⊢\top \to \surd :ℂ⟶ℂ$$
4	3	feqmptd	$$⊢\top \to \surd =\left(x\in ℂ⟼\sqrt{x}\right)$$
5	4	reseq1d	$$⊢\top \to {\surd \upharpoonright }_D={\left(x\in ℂ⟼\sqrt{x}\right)\upharpoonright }_D$$
6		difss	$$⊢ℂ\setminus \left(\mathrm{-\infty },0\right]\subseteq ℂ$$
7	1 6	eqsstri	$$⊢D\subseteq ℂ$$
8		resmpt	$$⊢D\subseteq ℂ\to {\left(x\in ℂ⟼\sqrt{x}\right)\upharpoonright }_D=\left(x\in D⟼\sqrt{x}\right)$$
9	7 8	mp1i	$$⊢\top \to {\left(x\in ℂ⟼\sqrt{x}\right)\upharpoonright }_D=\left(x\in D⟼\sqrt{x}\right)$$
10	7	sseli	$$⊢x\in D\to x\in ℂ$$
11	10	adantl	$$⊢\left(\top \wedge x\in D\right)\to x\in ℂ$$
12		cxpsqrt	$$⊢x\in ℂ\to x^{\frac{1}{2}}=\sqrt{x}$$
13	11 12	syl	$$⊢\left(\top \wedge x\in D\right)\to x^{\frac{1}{2}}=\sqrt{x}$$
14	13	eqcomd	$$⊢\left(\top \wedge x\in D\right)\to \sqrt{x}=x^{\frac{1}{2}}$$
15	14	mpteq2dva	$$⊢\top \to \left(x\in D⟼\sqrt{x}\right)=\left(x\in D⟼x^{\frac{1}{2}}\right)$$
16	5 9 15	3eqtrd	$$⊢\top \to {\surd \upharpoonright }_D=\left(x\in D⟼x^{\frac{1}{2}}\right)$$
17		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
18	17	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
19	18	a1i	$$⊢\top \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
20		resttopon	$$⊢\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge D\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\in \mathrm{TopOn}\left(D\right)$$
21	19 7 20	sylancl	$$⊢\top \to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\in \mathrm{TopOn}\left(D\right)$$
22	21	cnmptid	$$⊢\top \to \left(x\in D⟼x\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\right)$$
23		ax-1cn	$$⊢1\in ℂ$$
24		halfcl	$$⊢1\in ℂ\to \frac{1}{2}\in ℂ$$
25	23 24	mp1i	$$⊢\top \to \frac{1}{2}\in ℂ$$
26	21 19 25	cnmptc	$$⊢\top \to \left(x\in D⟼\frac{1}{2}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
27		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D$$
28	1 17 27	cxpcn	$$⊢\left(y\in D,z\in ℂ⟼y^z\right)\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
29	28	a1i	$$⊢\top \to \left(y\in D,z\in ℂ⟼y^z\right)\in \left(\left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
30		oveq12	$$⊢\left(y=x\wedge z=\frac{1}{2}\right)\to y^z=x^{\frac{1}{2}}$$
31	21 22 26 21 19 29 30	cnmpt12	$$⊢\top \to \left(x\in D⟼x^{\frac{1}{2}}\right)\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
32		ssid	$$⊢ℂ\subseteq ℂ$$
33	18	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
34	17 27 33	cncfcn	$$⊢\left(D\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to D\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
35	7 32 34	mp2an	$$⊢D\underset{cn}{⟶}ℂ=\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}D\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
36	31 35	eleqtrrdi	$$⊢\top \to \left(x\in D⟼x^{\frac{1}{2}}\right):D\underset{cn}{⟶}ℂ$$
37	16 36	eqeltrd	$$⊢\top \to \left({\surd \upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$
38	37	mptru	$$⊢\left({\surd \upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$