Metamath Proof Explorer

Theorem dvcnsqrt

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

Ref Expression
Hypothesis dvcncxp1.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion dvcnsqrt 
|- ( CC _D ( x e. D |-> ( sqrt ` x ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcncxp1.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 halfcn 
 |-  ( 1 / 2 ) e. CC
3 1 dvcncxp1 
 |-  ( ( 1 / 2 ) e. CC -> ( CC _D ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. D |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) )
4 2 3 ax-mp 
 |-  ( CC _D ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) ) = ( x e. D |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) )
5 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
6 1 5 eqsstri 
 |-  D C_ CC
7 6 sseli 
 |-  ( x e. D -> x e. CC )
8 cxpsqrt 
 |-  ( x e. CC -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
9 7 8 syl 
 |-  ( x e. D -> ( x ^c ( 1 / 2 ) ) = ( sqrt ` x ) )
10 9 mpteq2ia 
 |-  ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) = ( x e. D |-> ( sqrt ` x ) )
11 10 oveq2i 
 |-  ( CC _D ( x e. D |-> ( x ^c ( 1 / 2 ) ) ) ) = ( CC _D ( x e. D |-> ( sqrt ` x ) ) )
12 1p0e1 
 |-  ( 1 + 0 ) = 1
13 ax-1cn 
 |-  1 e. CC
14 2halves 
 |-  ( 1 e. CC -> ( ( 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 e. CC
18 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 ) ) ) )
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 
 |-  -u ( 1 / 2 ) = ( 0 - ( 1 / 2 ) )
22 20 21 eqtr4i 
 |-  ( ( 1 / 2 ) - 1 ) = -u ( 1 / 2 )
23 22 oveq2i 
 |-  ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( x ^c -u ( 1 / 2 ) )
24 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
25 2 a1i 
 |-  ( x e. D -> ( 1 / 2 ) e. CC )
26 7 24 25 cxpnegd 
 |-  ( x e. D -> ( x ^c -u ( 1 / 2 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) )
27 23 26 syl5eq 
 |-  ( x e. D -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( x ^c ( 1 / 2 ) ) ) )
28 9 oveq2d 
 |-  ( x e. D -> ( 1 / ( x ^c ( 1 / 2 ) ) ) = ( 1 / ( sqrt ` x ) ) )
29 27 28 eqtrd 
 |-  ( x e. D -> ( x ^c ( ( 1 / 2 ) - 1 ) ) = ( 1 / ( sqrt ` x ) ) )
30 29 oveq2d 
 |-  ( x e. D -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) )
31 1cnd 
 |-  ( x e. D -> 1 e. CC )
32 2cnd 
 |-  ( x e. D -> 2 e. CC )
33 7 sqrtcld 
 |-  ( x e. D -> ( sqrt ` x ) e. CC )
34 2ne0 
 |-  2 =/= 0
35 34 a1i 
 |-  ( x e. D -> 2 =/= 0 )
36 7 adantr 
 |-  ( ( x e. D /\ ( sqrt ` x ) = 0 ) -> x e. CC )
37 simpr 
 |-  ( ( x e. D /\ ( sqrt ` x ) = 0 ) -> ( sqrt ` x ) = 0 )
38 36 37 sqr00d 
 |-  ( ( x e. D /\ ( sqrt ` x ) = 0 ) -> x = 0 )
39 38 ex 
 |-  ( x e. D -> ( ( sqrt ` x ) = 0 -> x = 0 ) )
40 39 necon3d 
 |-  ( x e. D -> ( x =/= 0 -> ( sqrt ` x ) =/= 0 ) )
41 24 40 mpd 
 |-  ( x e. D -> ( sqrt ` x ) =/= 0 )
42 31 32 31 33 35 41 divmuldivd 
 |-  ( x e. D -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) )
43 1t1e1 
 |-  ( 1 x. 1 ) = 1
44 43 oveq1i 
 |-  ( ( 1 x. 1 ) / ( 2 x. ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) )
45 42 44 eqtrdi 
 |-  ( x e. D -> ( ( 1 / 2 ) x. ( 1 / ( sqrt ` x ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
46 30 45 eqtrd 
 |-  ( x e. D -> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) = ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
47 46 mpteq2ia 
 |-  ( x e. D |-> ( ( 1 / 2 ) x. ( x ^c ( ( 1 / 2 ) - 1 ) ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )
48 4 11 47 3eqtr3i 
 |-  ( CC _D ( x e. D |-> ( sqrt ` x ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqrt ` x ) ) ) )