Theorem dvcnsqrt

Description: Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018)

	Ref	Expression
Hypothesis	dvcncxp1.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	dvcnsqrt	$$⊢\frac{d\left(x\in D⟼\sqrt{x}\right)}{d_{ℂ}x}=\left(x\in D⟼\frac{1}{2\sqrt{x}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvcncxp1.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		halfcn	$$⊢\frac{1}{2}\in ℂ$$
3	1	dvcncxp1	$$⊢\frac{1}{2}\in ℂ\to \frac{d\left(x\in D⟼x^{\frac{1}{2}}\right)}{d_{ℂ}x}=\left(x\in D⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)$$
4	2 3	ax-mp	$$⊢\frac{d\left(x\in D⟼x^{\frac{1}{2}}\right)}{d_{ℂ}x}=\left(x\in D⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)$$
5		difss	$$⊢ℂ\setminus \left(\mathrm{-\infty },0\right]\subseteq ℂ$$
6	1 5	eqsstri	$$⊢D\subseteq ℂ$$
7	6	sseli	$$⊢x\in D\to x\in ℂ$$
8		cxpsqrt	$$⊢x\in ℂ\to x^{\frac{1}{2}}=\sqrt{x}$$
9	7 8	syl	$$⊢x\in D\to x^{\frac{1}{2}}=\sqrt{x}$$
10	9	mpteq2ia	$$⊢\left(x\in D⟼x^{\frac{1}{2}}\right)=\left(x\in D⟼\sqrt{x}\right)$$
11	10	oveq2i	$$⊢\frac{d\left(x\in D⟼x^{\frac{1}{2}}\right)}{d_{ℂ}x}=\frac{d\left(x\in D⟼\sqrt{x}\right)}{d_{ℂ}x}$$
12		1p0e1	$$⊢1+0=1$$
13		ax-1cn	$$⊢1\in ℂ$$
14		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
15	13 14	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
16	12 15	eqtr4i	$$⊢1+0=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
17		0cn	$$⊢0\in ℂ$$
18		addsubeq4	$$⊢\left(\left(1\in ℂ\wedge 0\in ℂ\right)\wedge \left(\frac{1}{2}\in ℂ\wedge \frac{1}{2}\in ℂ\right)\right)\to \left(1+0=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\leftrightarrow \left(\frac{1}{2}\right)-1=0-\left(\frac{1}{2}\right)\right)$$
19	13 17 2 2 18	mp4an	$$⊢1+0=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\leftrightarrow \left(\frac{1}{2}\right)-1=0-\left(\frac{1}{2}\right)$$
20	16 19	mpbi	$$⊢\left(\frac{1}{2}\right)-1=0-\left(\frac{1}{2}\right)$$
21		df-neg	$$⊢-\frac{1}{2}=0-\left(\frac{1}{2}\right)$$
22	20 21	eqtr4i	$$⊢\left(\frac{1}{2}\right)-1=-\frac{1}{2}$$
23	22	oveq2i	$$⊢x^{\left(\frac{1}{2}\right)-1}=x^{-\frac{1}{2}}$$
24	1	logdmn0	$$⊢x\in D\to x\ne 0$$
25	2	a1i	$$⊢x\in D\to \frac{1}{2}\in ℂ$$
26	7 24 25	cxpnegd	$$⊢x\in D\to x^{-\frac{1}{2}}=\frac{1}{x^{\frac{1}{2}}}$$
27	23 26	eqtrid	$$⊢x\in D\to x^{\left(\frac{1}{2}\right)-1}=\frac{1}{x^{\frac{1}{2}}}$$
28	9	oveq2d	$$⊢x\in D\to \frac{1}{x^{\frac{1}{2}}}=\frac{1}{\sqrt{x}}$$
29	27 28	eqtrd	$$⊢x\in D\to x^{\left(\frac{1}{2}\right)-1}=\frac{1}{\sqrt{x}}$$
30	29	oveq2d	$$⊢x\in D\to \left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}=\left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)$$
31		1cnd	$$⊢x\in D\to 1\in ℂ$$
32		2cnd	$$⊢x\in D\to 2\in ℂ$$
33	7	sqrtcld	$$⊢x\in D\to \sqrt{x}\in ℂ$$
34		2ne0	$$⊢2\ne 0$$
35	34	a1i	$$⊢x\in D\to 2\ne 0$$
36	7	adantr	$$⊢\left(x\in D\wedge \sqrt{x}=0\right)\to x\in ℂ$$
37		simpr	$$⊢\left(x\in D\wedge \sqrt{x}=0\right)\to \sqrt{x}=0$$
38	36 37	sqr00d	$$⊢\left(x\in D\wedge \sqrt{x}=0\right)\to x=0$$
39	38	ex	$$⊢x\in D\to \left(\sqrt{x}=0\to x=0\right)$$
40	39	necon3d	$$⊢x\in D\to \left(x\ne 0\to \sqrt{x}\ne 0\right)$$
41	24 40	mpd	$$⊢x\in D\to \sqrt{x}\ne 0$$
42	31 32 31 33 35 41	divmuldivd	$$⊢x\in D\to \left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)=\frac{1\cdot 1}{2\sqrt{x}}$$
43		1t1e1	$$⊢1\cdot 1=1$$
44	43	oveq1i	$$⊢\frac{1\cdot 1}{2\sqrt{x}}=\frac{1}{2\sqrt{x}}$$
45	42 44	eqtrdi	$$⊢x\in D\to \left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)=\frac{1}{2\sqrt{x}}$$
46	30 45	eqtrd	$$⊢x\in D\to \left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}=\frac{1}{2\sqrt{x}}$$
47	46	mpteq2ia	$$⊢\left(x\in D⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)=\left(x\in D⟼\frac{1}{2\sqrt{x}}\right)$$
48	4 11 47	3eqtr3i	$$⊢\frac{d\left(x\in D⟼\sqrt{x}\right)}{d_{ℂ}x}=\left(x\in D⟼\frac{1}{2\sqrt{x}}\right)$$