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 eqtrid 
 |-  ( 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 ) ) ) )