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

Metamath Proof Explorer

Theorem dvcxp2

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

Ref Expression
Assertion dvcxp2 
|- ( A e. RR+ -> ( CC _D ( x e. CC |-> ( A ^c x ) ) ) = ( x e. CC |-> ( ( log ` A ) x. ( A ^c x ) ) ) )

Proof

Step Hyp Ref Expression
1 cnelprrecn 
 |-  CC e. { RR , CC }
2 1 a1i 
 |-  ( A e. RR+ -> CC e. { RR , CC } )
3 simpr 
 |-  ( ( A e. RR+ /\ x e. CC ) -> x e. CC )
4 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
5 4 adantr 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( log ` A ) e. RR )
6 5 recnd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( log ` A ) e. CC )
7 3 6 mulcld 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( x x. ( log ` A ) ) e. CC )
8 efcl 
 |-  ( y e. CC -> ( exp ` y ) e. CC )
9 8 adantl 
 |-  ( ( A e. RR+ /\ y e. CC ) -> ( exp ` y ) e. CC )
10 3 6 mulcomd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( x x. ( log ` A ) ) = ( ( log ` A ) x. x ) )
11 10 mpteq2dva 
 |-  ( A e. RR+ -> ( x e. CC |-> ( x x. ( log ` A ) ) ) = ( x e. CC |-> ( ( log ` A ) x. x ) ) )
12 11 oveq2d 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( x x. ( log ` A ) ) ) ) = ( CC _D ( x e. CC |-> ( ( log ` A ) x. x ) ) ) )
13 1cnd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> 1 e. CC )
14 2 dvmptid 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
15 4 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
16 2 3 13 14 15 dvmptcmul 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( ( log ` A ) x. x ) ) ) = ( x e. CC |-> ( ( log ` A ) x. 1 ) ) )
17 6 mulridd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( ( log ` A ) x. 1 ) = ( log ` A ) )
18 17 mpteq2dva 
 |-  ( A e. RR+ -> ( x e. CC |-> ( ( log ` A ) x. 1 ) ) = ( x e. CC |-> ( log ` A ) ) )
19 12 16 18 3eqtrd 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( x x. ( log ` A ) ) ) ) = ( x e. CC |-> ( log ` A ) ) )
20 dvef 
 |-  ( CC _D exp ) = exp
21 eff 
 |-  exp : CC --> CC
22 21 a1i 
 |-  ( A e. RR+ -> exp : CC --> CC )
23 22 feqmptd 
 |-  ( A e. RR+ -> exp = ( y e. CC |-> ( exp ` y ) ) )
24 23 eqcomd 
 |-  ( A e. RR+ -> ( y e. CC |-> ( exp ` y ) ) = exp )
25 24 oveq2d 
 |-  ( A e. RR+ -> ( CC _D ( y e. CC |-> ( exp ` y ) ) ) = ( CC _D exp ) )
26 20 25 24 3eqtr4a 
 |-  ( A e. RR+ -> ( CC _D ( y e. CC |-> ( exp ` y ) ) ) = ( y e. CC |-> ( exp ` y ) ) )
27 fveq2 
 |-  ( y = ( x x. ( log ` A ) ) -> ( exp ` y ) = ( exp ` ( x x. ( log ` A ) ) ) )
28 2 2 7 5 9 9 19 26 27 27 dvmptco 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( exp ` ( x x. ( log ` A ) ) ) ) ) = ( x e. CC |-> ( ( exp ` ( x x. ( log ` A ) ) ) x. ( log ` A ) ) ) )
29 rpcn 
 |-  ( A e. RR+ -> A e. CC )
30 29 adantr 
 |-  ( ( A e. RR+ /\ x e. CC ) -> A e. CC )
31 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
32 31 adantr 
 |-  ( ( A e. RR+ /\ x e. CC ) -> A =/= 0 )
33 30 32 3 cxpefd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( A ^c x ) = ( exp ` ( x x. ( log ` A ) ) ) )
34 33 mpteq2dva 
 |-  ( A e. RR+ -> ( x e. CC |-> ( A ^c x ) ) = ( x e. CC |-> ( exp ` ( x x. ( log ` A ) ) ) ) )
35 34 oveq2d 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( A ^c x ) ) ) = ( CC _D ( x e. CC |-> ( exp ` ( x x. ( log ` A ) ) ) ) ) )
36 30 3 cxpcld 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( A ^c x ) e. CC )
37 6 36 mulcomd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( ( log ` A ) x. ( A ^c x ) ) = ( ( A ^c x ) x. ( log ` A ) ) )
38 33 oveq1d 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( ( A ^c x ) x. ( log ` A ) ) = ( ( exp ` ( x x. ( log ` A ) ) ) x. ( log ` A ) ) )
39 37 38 eqtrd 
 |-  ( ( A e. RR+ /\ x e. CC ) -> ( ( log ` A ) x. ( A ^c x ) ) = ( ( exp ` ( x x. ( log ` A ) ) ) x. ( log ` A ) ) )
40 39 mpteq2dva 
 |-  ( A e. RR+ -> ( x e. CC |-> ( ( log ` A ) x. ( A ^c x ) ) ) = ( x e. CC |-> ( ( exp ` ( x x. ( log ` A ) ) ) x. ( log ` A ) ) ) )
41 28 35 40 3eqtr4d 
 |-  ( A e. RR+ -> ( CC _D ( x e. CC |-> ( A ^c x ) ) ) = ( x e. CC |-> ( ( log ` A ) x. ( A ^c x ) ) ) )