Metamath Proof Explorer


Theorem dvcnsqrt

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

Ref Expression
Hypothesis dvcncxp1.d D = −∞ 0
Assertion dvcnsqrt dx D x d x = x D 1 2 x

Proof

Step Hyp Ref Expression
1 dvcncxp1.d D = −∞ 0
2 halfcn 1 2
3 1 dvcncxp1 1 2 dx D x 1 2 d x = x D 1 2 x 1 2 1
4 2 3 ax-mp dx D x 1 2 d x = x D 1 2 x 1 2 1
5 difss −∞ 0
6 1 5 eqsstri D
7 6 sseli x D x
8 cxpsqrt x x 1 2 = x
9 7 8 syl x D x 1 2 = x
10 9 mpteq2ia x D x 1 2 = x D x
11 10 oveq2i dx D x 1 2 d x = dx D x d x
12 1p0e1 1 + 0 = 1
13 ax-1cn 1
14 2halves 1 1 2 + 1 2 = 1
15 13 14 ax-mp 1 2 + 1 2 = 1
16 12 15 eqtr4i 1 + 0 = 1 2 + 1 2
17 0cn 0
18 addsubeq4 1 0 1 2 1 2 1 + 0 = 1 2 + 1 2 1 2 1 = 0 1 2
19 13 17 2 2 18 mp4an 1 + 0 = 1 2 + 1 2 1 2 1 = 0 1 2
20 16 19 mpbi 1 2 1 = 0 1 2
21 df-neg 1 2 = 0 1 2
22 20 21 eqtr4i 1 2 1 = 1 2
23 22 oveq2i x 1 2 1 = x 1 2
24 1 logdmn0 x D x 0
25 2 a1i x D 1 2
26 7 24 25 cxpnegd x D x 1 2 = 1 x 1 2
27 23 26 syl5eq x D x 1 2 1 = 1 x 1 2
28 9 oveq2d x D 1 x 1 2 = 1 x
29 27 28 eqtrd x D x 1 2 1 = 1 x
30 29 oveq2d x D 1 2 x 1 2 1 = 1 2 1 x
31 1cnd x D 1
32 2cnd x D 2
33 7 sqrtcld x D x
34 2ne0 2 0
35 34 a1i x D 2 0
36 7 adantr x D x = 0 x
37 simpr x D x = 0 x = 0
38 36 37 sqr00d x D x = 0 x = 0
39 38 ex x D x = 0 x = 0
40 39 necon3d x D x 0 x 0
41 24 40 mpd x D x 0
42 31 32 31 33 35 41 divmuldivd x D 1 2 1 x = 1 1 2 x
43 1t1e1 1 1 = 1
44 43 oveq1i 1 1 2 x = 1 2 x
45 42 44 eqtrdi x D 1 2 1 x = 1 2 x
46 30 45 eqtrd x D 1 2 x 1 2 1 = 1 2 x
47 46 mpteq2ia x D 1 2 x 1 2 1 = x D 1 2 x
48 4 11 47 3eqtr3i dx D x d x = x D 1 2 x