This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvcxp1

Description: The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Assertion dvcxp1 
|- ( A e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c A ) ) ) = ( x e. RR+ |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 reelprrecn 
 |-  RR e. { RR , CC }
2 1 a1i 
 |-  ( A e. CC -> RR e. { RR , CC } )
3 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
4 3 adantl 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( log ` x ) e. RR )
5 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
6 5 adantl 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
7 recn 
 |-  ( y e. RR -> y e. CC )
8 mulcl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( A x. y ) e. CC )
9 efcl 
 |-  ( ( A x. y ) e. CC -> ( exp ` ( A x. y ) ) e. CC )
10 8 9 syl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( exp ` ( A x. y ) ) e. CC )
11 7 10 sylan2 
 |-  ( ( A e. CC /\ y e. RR ) -> ( exp ` ( A x. y ) ) e. CC )
12 ovexd 
 |-  ( ( A e. CC /\ y e. RR ) -> ( ( exp ` ( A x. y ) ) x. A ) e. _V )
13 relogf1o 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR
14 f1of 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR -> ( log |` RR+ ) : RR+ --> RR )
15 13 14 mp1i 
 |-  ( A e. CC -> ( log |` RR+ ) : RR+ --> RR )
16 15 feqmptd 
 |-  ( A e. CC -> ( log |` RR+ ) = ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) )
17 fvres 
 |-  ( x e. RR+ -> ( ( log |` RR+ ) ` x ) = ( log ` x ) )
18 17 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( log |` RR+ ) ` x ) ) = ( x e. RR+ |-> ( log ` x ) )
19 16 18 eqtrdi 
 |-  ( A e. CC -> ( log |` RR+ ) = ( x e. RR+ |-> ( log ` x ) ) )
20 19 oveq2d 
 |-  ( A e. CC -> ( RR _D ( log |` RR+ ) ) = ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) )
21 dvrelog 
 |-  ( RR _D ( log |` RR+ ) ) = ( x e. RR+ |-> ( 1 / x ) )
22 20 21 eqtr3di 
 |-  ( A e. CC -> ( RR _D ( x e. RR+ |-> ( log ` x ) ) ) = ( x e. RR+ |-> ( 1 / x ) ) )
23 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
24 23 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
25 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
26 24 25 mp1i 
 |-  ( A e. CC -> CC e. ( TopOpen ` CCfld ) )
27 ax-resscn 
 |-  RR C_ CC
28 27 a1i 
 |-  ( A e. CC -> RR C_ CC )
29 dfss2 
 |-  ( RR C_ CC <-> ( RR i^i CC ) = RR )
30 28 29 sylib 
 |-  ( A e. CC -> ( RR i^i CC ) = RR )
31 ovexd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( exp ` ( A x. y ) ) x. A ) e. _V )
32 cnelprrecn 
 |-  CC e. { RR , CC }
33 32 a1i 
 |-  ( A e. CC -> CC e. { RR , CC } )
34 simpl 
 |-  ( ( A e. CC /\ y e. CC ) -> A e. CC )
35 efcl 
 |-  ( x e. CC -> ( exp ` x ) e. CC )
36 35 adantl 
 |-  ( ( A e. CC /\ x e. CC ) -> ( exp ` x ) e. CC )
37 simpr 
 |-  ( ( A e. CC /\ y e. CC ) -> y e. CC )
38 1cnd 
 |-  ( ( A e. CC /\ y e. CC ) -> 1 e. CC )
39 33 dvmptid 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
40 id 
 |-  ( A e. CC -> A e. CC )
41 33 37 38 39 40 dvmptcmul 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( A x. y ) ) ) = ( y e. CC |-> ( A x. 1 ) ) )
42 mulrid 
 |-  ( A e. CC -> ( A x. 1 ) = A )
43 42 mpteq2dv 
 |-  ( A e. CC -> ( y e. CC |-> ( A x. 1 ) ) = ( y e. CC |-> A ) )
44 41 43 eqtrd 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( A x. y ) ) ) = ( y e. CC |-> A ) )
45 dvef 
 |-  ( CC _D exp ) = exp
46 eff 
 |-  exp : CC --> CC
47 46 a1i 
 |-  ( A e. CC -> exp : CC --> CC )
48 47 feqmptd 
 |-  ( A e. CC -> exp = ( x e. CC |-> ( exp ` x ) ) )
49 48 eqcomd 
 |-  ( A e. CC -> ( x e. CC |-> ( exp ` x ) ) = exp )
50 49 oveq2d 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( exp ` x ) ) ) = ( CC _D exp ) )
51 45 50 49 3eqtr4a 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( exp ` x ) ) ) = ( x e. CC |-> ( exp ` x ) ) )
52 fveq2 
 |-  ( x = ( A x. y ) -> ( exp ` x ) = ( exp ` ( A x. y ) ) )
53 33 33 8 34 36 36 44 51 52 52 dvmptco 
 |-  ( A e. CC -> ( CC _D ( y e. CC |-> ( exp ` ( A x. y ) ) ) ) = ( y e. CC |-> ( ( exp ` ( A x. y ) ) x. A ) ) )
54 23 2 26 30 10 31 53 dvmptres3 
 |-  ( A e. CC -> ( RR _D ( y e. RR |-> ( exp ` ( A x. y ) ) ) ) = ( y e. RR |-> ( ( exp ` ( A x. y ) ) x. A ) ) )
55 oveq2 
 |-  ( y = ( log ` x ) -> ( A x. y ) = ( A x. ( log ` x ) ) )
56 55 fveq2d 
 |-  ( y = ( log ` x ) -> ( exp ` ( A x. y ) ) = ( exp ` ( A x. ( log ` x ) ) ) )
57 56 oveq1d 
 |-  ( y = ( log ` x ) -> ( ( exp ` ( A x. y ) ) x. A ) = ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) )
58 2 2 4 6 11 12 22 54 56 57 dvmptco 
 |-  ( A e. CC -> ( RR _D ( x e. RR+ |-> ( exp ` ( A x. ( log ` x ) ) ) ) ) = ( x e. RR+ |-> ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) ) )
59 rpcn 
 |-  ( x e. RR+ -> x e. CC )
60 59 adantl 
 |-  ( ( A e. CC /\ x e. RR+ ) -> x e. CC )
61 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
62 61 adantl 
 |-  ( ( A e. CC /\ x e. RR+ ) -> x =/= 0 )
63 simpl 
 |-  ( ( A e. CC /\ x e. RR+ ) -> A e. CC )
64 60 62 63 cxpefd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( x ^c A ) = ( exp ` ( A x. ( log ` x ) ) ) )
65 64 mpteq2dva 
 |-  ( A e. CC -> ( x e. RR+ |-> ( x ^c A ) ) = ( x e. RR+ |-> ( exp ` ( A x. ( log ` x ) ) ) ) )
66 65 oveq2d 
 |-  ( A e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c A ) ) ) = ( RR _D ( x e. RR+ |-> ( exp ` ( A x. ( log ` x ) ) ) ) ) )
67 1cnd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> 1 e. CC )
68 60 62 63 67 cxpsubd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( x ^c ( A - 1 ) ) = ( ( x ^c A ) / ( x ^c 1 ) ) )
69 60 cxp1d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( x ^c 1 ) = x )
70 69 oveq2d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( x ^c A ) / ( x ^c 1 ) ) = ( ( x ^c A ) / x ) )
71 60 63 cxpcld 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( x ^c A ) e. CC )
72 71 60 62 divrecd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( x ^c A ) / x ) = ( ( x ^c A ) x. ( 1 / x ) ) )
73 68 70 72 3eqtrd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( x ^c ( A - 1 ) ) = ( ( x ^c A ) x. ( 1 / x ) ) )
74 73 oveq2d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( A x. ( x ^c ( A - 1 ) ) ) = ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) )
75 6 rpcnd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( 1 / x ) e. CC )
76 63 71 75 mul12d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) = ( ( x ^c A ) x. ( A x. ( 1 / x ) ) ) )
77 71 63 75 mulassd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) = ( ( x ^c A ) x. ( A x. ( 1 / x ) ) ) )
78 76 77 eqtr4d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( A x. ( ( x ^c A ) x. ( 1 / x ) ) ) = ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) )
79 64 oveq1d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( x ^c A ) x. A ) = ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) )
80 79 oveq1d 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( ( ( x ^c A ) x. A ) x. ( 1 / x ) ) = ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) )
81 74 78 80 3eqtrd 
 |-  ( ( A e. CC /\ x e. RR+ ) -> ( A x. ( x ^c ( A - 1 ) ) ) = ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) )
82 81 mpteq2dva 
 |-  ( A e. CC -> ( x e. RR+ |-> ( A x. ( x ^c ( A - 1 ) ) ) ) = ( x e. RR+ |-> ( ( ( exp ` ( A x. ( log ` x ) ) ) x. A ) x. ( 1 / x ) ) ) )
83 58 66 82 3eqtr4d 
 |-  ( A e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c A ) ) ) = ( x e. RR+ |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )