Theorem dvsqrt

Description: The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016)

	Ref	Expression
Assertion	dvsqrt	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼\sqrt{x}\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{2\sqrt{x}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		halfcn	$$⊢\frac{1}{2}\in ℂ$$
2		dvcxp1	$$⊢\frac{1}{2}\in ℂ\to \frac{d\left(x\in {ℝ}^{+}⟼x^{\frac{1}{2}}\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)$$
3	1 2	ax-mp	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼x^{\frac{1}{2}}\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)$$
4		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
5		cxpsqrt	$$⊢x\in ℂ\to x^{\frac{1}{2}}=\sqrt{x}$$
6	4 5	syl	$$⊢x\in {ℝ}^{+}\to x^{\frac{1}{2}}=\sqrt{x}$$
7	6	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼x^{\frac{1}{2}}\right)=\left(x\in {ℝ}^{+}⟼\sqrt{x}\right)$$
8	7	oveq2i	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼x^{\frac{1}{2}}\right)}{d_{ℝ}x}=\frac{d\left(x\in {ℝ}^{+}⟼\sqrt{x}\right)}{d_{ℝ}x}$$
9		1p0e1	$$⊢1+0=1$$
10		ax-1cn	$$⊢1\in ℂ$$
11		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
12	10 11	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
13	9 12	eqtr4i	$$⊢1+0=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
14		0cn	$$⊢0\in ℂ$$
15		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)$$
16	10 14 1 1 15	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)$$
17	13 16	mpbi	$$⊢\left(\frac{1}{2}\right)-1=0-\left(\frac{1}{2}\right)$$
18		df-neg	$$⊢-\frac{1}{2}=0-\left(\frac{1}{2}\right)$$
19	17 18	eqtr4i	$$⊢\left(\frac{1}{2}\right)-1=-\frac{1}{2}$$
20	19	oveq2i	$$⊢x^{\left(\frac{1}{2}\right)-1}=x^{-\frac{1}{2}}$$
21		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
22	1	a1i	$$⊢x\in {ℝ}^{+}\to \frac{1}{2}\in ℂ$$
23	4 21 22	cxpnegd	$$⊢x\in {ℝ}^{+}\to x^{-\frac{1}{2}}=\frac{1}{x^{\frac{1}{2}}}$$
24	20 23	syl5eq	$$⊢x\in {ℝ}^{+}\to x^{\left(\frac{1}{2}\right)-1}=\frac{1}{x^{\frac{1}{2}}}$$
25	6	oveq2d	$$⊢x\in {ℝ}^{+}\to \frac{1}{x^{\frac{1}{2}}}=\frac{1}{\sqrt{x}}$$
26	24 25	eqtrd	$$⊢x\in {ℝ}^{+}\to x^{\left(\frac{1}{2}\right)-1}=\frac{1}{\sqrt{x}}$$
27	26	oveq2d	$$⊢x\in {ℝ}^{+}\to \left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}=\left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)$$
28	10	a1i	$$⊢x\in {ℝ}^{+}\to 1\in ℂ$$
29		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
30	29	a1i	$$⊢x\in {ℝ}^{+}\to \left(2\in ℂ\wedge 2\ne 0\right)$$
31		rpsqrtcl	$$⊢x\in {ℝ}^{+}\to \sqrt{x}\in {ℝ}^{+}$$
32	31	rpcnne0d	$$⊢x\in {ℝ}^{+}\to \left(\sqrt{x}\in ℂ\wedge \sqrt{x}\ne 0\right)$$
33		divmuldiv	$$⊢\left(\left(1\in ℂ\wedge 1\in ℂ\right)\wedge \left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\sqrt{x}\in ℂ\wedge \sqrt{x}\ne 0\right)\right)\right)\to \left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)=\frac{1\cdot 1}{2\sqrt{x}}$$
34	28 28 30 32 33	syl22anc	$$⊢x\in {ℝ}^{+}\to \left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)=\frac{1\cdot 1}{2\sqrt{x}}$$
35		1t1e1	$$⊢1\cdot 1=1$$
36	35	oveq1i	$$⊢\frac{1\cdot 1}{2\sqrt{x}}=\frac{1}{2\sqrt{x}}$$
37	34 36	eqtrdi	$$⊢x\in {ℝ}^{+}\to \left(\frac{1}{2}\right)\left(\frac{1}{\sqrt{x}}\right)=\frac{1}{2\sqrt{x}}$$
38	27 37	eqtrd	$$⊢x\in {ℝ}^{+}\to \left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}=\frac{1}{2\sqrt{x}}$$
39	38	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left(\frac{1}{2}\right)x^{\left(\frac{1}{2}\right)-1}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{2\sqrt{x}}\right)$$
40	3 8 39	3eqtr3i	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼\sqrt{x}\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{2\sqrt{x}}\right)$$