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