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