Metamath Proof Explorer

Theorem dvcncxp1

Description: Derivative of complex power with respect to first argument on the complex plane. (Contributed by Brendan Leahy, 18-Dec-2018)

Ref Expression
Hypothesis dvcncxp1.d 
|- D = ( CC \ ( -oo (,] 0 ) )
Assertion dvcncxp1 
|- ( A e. CC -> ( CC _D ( x e. D |-> ( x ^c A ) ) ) = ( x e. D |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvcncxp1.d 
 |-  D = ( CC \ ( -oo (,] 0 ) )
2 cnelprrecn 
 |-  CC e. { RR , CC }
3 2 a1i 
 |-  ( A e. CC -> CC e. { RR , CC } )
4 difss 
 |-  ( CC \ ( -oo (,] 0 ) ) C_ CC
5 1 4 eqsstri 
 |-  D C_ CC
6 5 sseli 
 |-  ( x e. D -> x e. CC )
7 1 logdmn0 
 |-  ( x e. D -> x =/= 0 )
8 6 7 logcld 
 |-  ( x e. D -> ( log ` x ) e. CC )
9 8 adantl 
 |-  ( ( A e. CC /\ x e. D ) -> ( log ` x ) e. CC )
10 6 7 reccld 
 |-  ( x e. D -> ( 1 / x ) e. CC )
11 10 adantl 
 |-  ( ( A e. CC /\ x e. D ) -> ( 1 / x ) e. CC )
12 mulcl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( A x. y ) e. CC )
13 efcl 
 |-  ( ( A x. y ) e. CC -> ( exp ` ( A x. y ) ) e. CC )
14 12 13 syl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( exp ` ( A x. y ) ) e. CC )
15 ovexd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( exp ` ( A x. y ) ) x. A ) e. _V )
16 1 logcn 
 |-  ( log |` D ) e. ( D -cn-> CC )
17 cncff 
 |-  ( ( log |` D ) e. ( D -cn-> CC ) -> ( log |` D ) : D --> CC )
18 16 17 mp1i 
 |-  ( A e. CC -> ( log |` D ) : D --> CC )
19 18 feqmptd 
 |-  ( A e. CC -> ( log |` D ) = ( x e. D |-> ( ( log |` D ) ` x ) ) )
20 fvres 
 |-  ( x e. D -> ( ( log |` D ) ` x ) = ( log ` x ) )
21 20 mpteq2ia 
 |-  ( x e. D |-> ( ( log |` D ) ` x ) ) = ( x e. D |-> ( log ` x ) )
22 19 21 eqtrdi 
 |-  ( A e. CC -> ( log |` D ) = ( x e. D |-> ( log ` x ) ) )
23 22 oveq2d 
 |-  ( A e. CC -> ( CC _D ( log |` D ) ) = ( CC _D ( x e. D |-> ( log ` x ) ) ) )
24 1 dvlog 
 |-  ( CC _D ( log |` D ) ) = ( x e. D |-> ( 1 / x ) )
25 23 24 eqtr3di 
 |-  ( A e. CC -> ( CC _D ( x e. D |-> ( log ` x ) ) ) = ( x e. D |-> ( 1 / x ) ) )
26 simpl 
 |-  ( ( A e. CC /\ y e. CC ) -> A e. CC )
27 efcl 
 |-  ( x e. CC -> ( exp ` x ) e. CC )
28 27 adantl 
 |-  ( ( A e. CC /\ x e. CC ) -> ( exp ` x ) e. CC )
29 simpr 
 |-  ( ( A e. CC /\ y e. CC ) -> y e. CC )
30 1cnd 
 |-  ( ( A e. CC /\ y e. CC ) -> 1 e. CC )
31 3 dvmptid 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
32 id 
 |-  ( A e. CC -> A e. CC )
33 3 29 30 31 32 dvmptcmul 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( A x. y ) ) ) = ( y e. CC |-> ( A x. 1 ) ) )
34 mulrid 
 |-  ( A e. CC -> ( A x. 1 ) = A )
35 34 mpteq2dv 
 |-  ( A e. CC -> ( y e. CC |-> ( A x. 1 ) ) = ( y e. CC |-> A ) )
36 33 35 eqtrd 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( A x. y ) ) ) = ( y e. CC |-> A ) )
37 dvef 
 |-  ( CC _D exp ) = exp
38 eff 
 |-  exp : CC --> CC
39 38 a1i 
 |-  ( A e. CC -> exp : CC --> CC )
40 39 feqmptd 
 |-  ( A e. CC -> exp = ( x e. CC |-> ( exp ` x ) ) )
41 40 oveq2d 
 |-  ( A e. CC -> ( CC _D exp ) = ( CC _D ( x e. CC |-> ( exp ` x ) ) ) )
42 37 41 40 3eqtr3a 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( exp ` x ) ) ) = ( x e. CC |-> ( exp ` x ) ) )
43 fveq2 
 |-  ( x = ( A x. y ) -> ( exp ` x ) = ( exp ` ( A x. y ) ) )
44 3 3 12 26 28 28 36 42 43 43 dvmptco 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( exp ` ( A x. y ) ) ) ) = ( y e. CC |-> ( ( exp ` ( A x. y ) ) x. A ) ) )
45 oveq2 
 |-  ( y = ( log ` x ) -> ( A x. y ) = ( A x. ( log ` x ) ) )
46 45 fveq2d 
 |-  ( y = ( log ` x ) -> ( exp ` ( A x. y ) ) = ( exp ` ( A x. ( log ` x ) ) ) )
47 46 oveq1d 
 |-  ( y = ( log ` x ) -> ( ( exp ` ( A x. y ) ) x. A ) = ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) )
48 3 3 9 11 14 15 25 44 46 47 dvmptco 
 |-  ( A e. CC -> ( CC _D ( x e. D |-> ( exp ` ( A x. ( log ` x ) ) ) ) ) = ( x e. D |-> ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) ) )
49 6 adantl 
 |-  ( ( A e. CC /\ x e. D ) -> x e. CC )
50 7 adantl 
 |-  ( ( A e. CC /\ x e. D ) -> x =/= 0 )
51 simpl 
 |-  ( ( A e. CC /\ x e. D ) -> A e. CC )
52 49 50 51 cxpefd 
 |-  ( ( A e. CC /\ x e. D ) -> ( x ^c A ) = ( exp ` ( A x. ( log ` x ) ) ) )
53 52 mpteq2dva 
 |-  ( A e. CC -> ( x e. D |-> ( x ^c A ) ) = ( x e. D |-> ( exp ` ( A x. ( log ` x ) ) ) ) )
54 53 oveq2d 
 |-  ( A e. CC -> ( CC _D ( x e. D |-> ( x ^c A ) ) ) = ( CC _D ( x e. D |-> ( exp ` ( A x. ( log ` x ) ) ) ) ) )
55 1cnd 
 |-  ( ( A e. CC /\ x e. D ) -> 1 e. CC )
56 49 50 51 55 cxpsubd 
 |-  ( ( A e. CC /\ x e. D ) -> ( x ^c ( A - 1 ) ) = ( ( x ^c A ) / ( x ^c 1 ) ) )
57 49 cxp1d 
 |-  ( ( A e. CC /\ x e. D ) -> ( x ^c 1 ) = x )
58 57 oveq2d 
 |-  ( ( A e. CC /\ x e. D ) -> ( ( x ^c A ) / ( x ^c 1 ) ) = ( ( x ^c A ) / x ) )
59 49 51 cxpcld 
 |-  ( ( A e. CC /\ x e. D ) -> ( x ^c A ) e. CC )
60 59 49 50 divrecd 
 |-  ( ( A e. CC /\ x e. D ) -> ( ( x ^c A ) / x ) = ( ( x ^c A ) x. ( 1 / x ) ) )
61 56 58 60 3eqtrd 
 |-  ( ( A e. CC /\ x e. D ) -> ( x ^c ( A - 1 ) ) = ( ( x ^c A ) x. ( 1 / x ) ) )
62 61 oveq2d 
 |-  ( ( A e. CC /\ x e. D ) -> ( A x. ( x ^c ( A - 1 ) ) ) = ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) )
63 51 59 11 mul12d 
 |-  ( ( A e. CC /\ x e. D ) -> ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) = ( ( x ^c A ) x. ( A x. ( 1 / x ) ) ) )
64 59 51 11 mulassd 
 |-  ( ( A e. CC /\ x e. D ) -> ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) = ( ( x ^c A ) x. ( A x. ( 1 / x ) ) ) )
65 63 64 eqtr4d 
 |-  ( ( A e. CC /\ x e. D ) -> ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) = ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) )
66 52 oveq1d 
 |-  ( ( A e. CC /\ x e. D ) -> ( ( x ^c A ) x. A ) = ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) )
67 66 oveq1d 
 |-  ( ( A e. CC /\ x e. D ) -> ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) = ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) )
68 62 65 67 3eqtrd 
 |-  ( ( A e. CC /\ x e. D ) -> ( A x. ( x ^c ( A - 1 ) ) ) = ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) )
69 68 mpteq2dva 
 |-  ( A e. CC -> ( x e. D |-> ( A x. ( x ^c ( A - 1 ) ) ) ) = ( x e. D |-> ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) ) )
70 48 54 69 3eqtr4d 
 |-  ( A e. CC -> ( CC _D ( x e. D |-> ( x ^c A ) ) ) = ( x e. D |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )