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\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼A^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\log A{A}^x\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
2	1	a1i	$$⊢A\in {ℝ}^{+}\to ℂ\in \left\{ℝ,ℂ\right\}$$
3		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to x\in ℂ$$
4		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
5	4	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to \log A\in ℝ$$
6	5	recnd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to \log A\in ℂ$$
7	3 6	mulcld	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to x\log A\in ℂ$$
8		efcl	$$⊢y\in ℂ\to {\mathrm{e}}^y\in ℂ$$
9	8	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge y\in ℂ\right)\to {\mathrm{e}}^y\in ℂ$$
10	3 6	mulcomd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to x\log A=\log Ax$$
11	10	mpteq2dva	$$⊢A\in {ℝ}^{+}\to \left(x\in ℂ⟼x\log A\right)=\left(x\in ℂ⟼\log Ax\right)$$
12	11	oveq2d	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼x\log A\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼\log Ax\right)}{d_{ℂ}x}$$
13		1cnd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to 1\in ℂ$$
14	2	dvmptid	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1\right)$$
15	4	recnd	$$⊢A\in {ℝ}^{+}\to \log A\in ℂ$$
16	2 3 13 14 15	dvmptcmul	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼\log Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\log A\cdot 1\right)$$
17	6	mulid1d	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to \log A\cdot 1=\log A$$
18	17	mpteq2dva	$$⊢A\in {ℝ}^{+}\to \left(x\in ℂ⟼\log A\cdot 1\right)=\left(x\in ℂ⟼\log A\right)$$
19	12 16 18	3eqtrd	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼x\log A\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\log A\right)$$
20		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
21		eff	$$⊢\exp :ℂ⟶ℂ$$
22	21	a1i	$$⊢A\in {ℝ}^{+}\to \exp :ℂ⟶ℂ$$
23	22	feqmptd	$$⊢A\in {ℝ}^{+}\to \exp =\left(y\in ℂ⟼{\mathrm{e}}^y\right)$$
24	23	eqcomd	$$⊢A\in {ℝ}^{+}\to \left(y\in ℂ⟼{\mathrm{e}}^y\right)=\exp$$
25	24	oveq2d	$$⊢A\in {ℝ}^{+}\to \frac{d\left(y\in ℂ⟼{\mathrm{e}}^y\right)}{d_{ℂ}y}=ℂ\mathrm{D}\exp$$
26	20 25 24	3eqtr4a	$$⊢A\in {ℝ}^{+}\to \frac{d\left(y\in ℂ⟼{\mathrm{e}}^y\right)}{d_{ℂ}y}=\left(y\in ℂ⟼{\mathrm{e}}^y\right)$$
27		fveq2	$$⊢y=x\log A\to {\mathrm{e}}^y={\mathrm{e}}^{x\log A}$$
28	2 2 7 5 9 9 19 26 27 27	dvmptco	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼{\mathrm{e}}^{x\log A}\right)}{d_{ℂ}x}=\left(x\in ℂ⟼{\mathrm{e}}^{x\log A}\log A\right)$$
29		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
30	29	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to A\in ℂ$$
31		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
32	31	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to A\ne 0$$
33	30 32 3	cxpefd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to A^x={\mathrm{e}}^{x\log A}$$
34	33	mpteq2dva	$$⊢A\in {ℝ}^{+}\to \left(x\in ℂ⟼A^x\right)=\left(x\in ℂ⟼{\mathrm{e}}^{x\log A}\right)$$
35	34	oveq2d	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼A^x\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼{\mathrm{e}}^{x\log A}\right)}{d_{ℂ}x}$$
36	30 3	cxpcld	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to A^x\in ℂ$$
37	6 36	mulcomd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to \log A{A}^x=A^x\log A$$
38	33	oveq1d	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to A^x\log A={\mathrm{e}}^{x\log A}\log A$$
39	37 38	eqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge x\in ℂ\right)\to \log A{A}^x={\mathrm{e}}^{x\log A}\log A$$
40	39	mpteq2dva	$$⊢A\in {ℝ}^{+}\to \left(x\in ℂ⟼\log A{A}^x\right)=\left(x\in ℂ⟼{\mathrm{e}}^{x\log A}\log A\right)$$
41	28 35 40	3eqtr4d	$$⊢A\in {ℝ}^{+}\to \frac{d\left(x\in ℂ⟼A^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\log A{A}^x\right)$$