Metamath Proof Explorer


Theorem dvsqrt

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

Ref Expression
Assertion dvsqrt
|- ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 halfcn
 |-  ( 1 / 2 ) e. CC
2 dvcxp1
 |-  ( ( 1 / 2 ) e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) )
3 1 2 ax-mp
 |-  ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) )
4 rpcn
 |-  ( x e. RR+ -> x e. CC )
5 cxpsqrt
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
6 4 5 syl
 |-  ( x e. RR+ -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
7 6 mpteq2ia
 |-  ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) = ( x e. RR+ |-> ( sqrt ` x ) )
8 7 oveq2i
 |-  ( RR _D ( x e. RR+ |-> ( x ^c ( 1 / 2 ) ) ) ) = ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) )
9 1p0e1
 |-  ( 1 + 0 ) = 1
10 ax-1cn
 |-  1 e. CC
11 2halves
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
12 10 11 ax-mp
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
13 9 12 eqtr4i
 |-  ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) )
14 0cn
 |-  0 e. CC
15 addsubeq4
 |-  ( ( ( 1 e. CC /\ 0 e. CC ) /\ ( ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) ) -> ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) <-> ( ( 1 / 2 ) - 1 ) = ( 0 - ( 1 / 2 ) ) ) )
16 10 14 1 1 15 mp4an
 |-  ( ( 1 + 0 ) = ( ( 1 / 2 ) + ( 1 / 2 ) ) <-> ( ( 1 / 2 ) - 1 ) = ( 0 - ( 1 / 2 ) ) )
17 13 16 mpbi
 |-  ( ( 1 / 2 ) - 1 ) = ( 0 - ( 1 / 2 ) )
18 df-neg
 |-  -u ( 1 / 2 ) = ( 0 - ( 1 / 2 ) )
19 17 18 eqtr4i
 |-  ( ( 1 / 2 ) - 1 ) = -u ( 1 / 2 )
20 19 oveq2i
 |-  ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( x ^c -u ( 1 / 2 ) )
21 rpne0
 |-  ( x e. RR+ -> x =/= 0 )
22 1 a1i
 |-  ( x e. RR+ -> ( 1 / 2 ) e. CC )
23 4 21 22 cxpnegd
 |-  ( x e. RR+ -> ( x ^c -u ( 1 / 2 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) )
24 20 23 syl5eq
 |-  ( x e. RR+ -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) )
25 6 oveq2d
 |-  ( x e. RR+ -> ( 1 / ( x ^c ( 1 / 2 ) ) ) = ( 1 / ( sqrt ` x ) ) )
26 24 25 eqtrd
 |-  ( x e. RR+ -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( sqrt ` x ) ) )
27 26 oveq2d
 |-  ( x e. RR+ -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) )
28 10 a1i
 |-  ( x e. RR+ -> 1 e. CC )
29 2cnne0
 |-  ( 2 e. CC /\ 2 =/= 0 )
30 29 a1i
 |-  ( x e. RR+ -> ( 2 e. CC /\ 2 =/= 0 ) )
31 rpsqrtcl
 |-  ( x e. RR+ -> ( sqrt ` x ) e. RR+ )
32 31 rpcnne0d
 |-  ( x e. RR+ -> ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) )
33 divmuldiv
 |-  ( ( ( 1 e. CC /\ 1 e. CC ) /\ ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( sqrt ` x ) e. CC /\ ( sqrt ` x ) =/= 0 ) ) ) -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) )
34 28 28 30 32 33 syl22anc
 |-  ( x e. RR+ -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) )
35 1t1e1
 |-  ( 1 x. 1 ) = 1
36 35 oveq1i
 |-  ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) )
37 34 36 eqtrdi
 |-  ( x e. RR+ -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
38 27 37 eqtrd
 |-  ( x e. RR+ -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
39 38 mpteq2ia
 |-  ( x e. RR+ |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
40 3 8 39 3eqtr3i
 |-  ( RR _D ( x e. RR+ |-> ( sqrt ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )