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=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	dvcncxp1	$$⊢A\in ℂ\to \frac{d\left(x\in D⟼x^A\right)}{d_{ℂ}x}=\left(x\in D⟼A{x}^{A-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvcncxp1.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
3	2	a1i	$$⊢A\in ℂ\to ℂ\in \left\{ℝ,ℂ\right\}$$
4		difss	$$⊢ℂ\setminus \left(\mathrm{-\infty },0\right]\subseteq ℂ$$
5	1 4	eqsstri	$$⊢D\subseteq ℂ$$
6	5	sseli	$$⊢x\in D\to x\in ℂ$$
7	1	logdmn0	$$⊢x\in D\to x\ne 0$$
8	6 7	logcld	$$⊢x\in D\to \log x\in ℂ$$
9	8	adantl	$$⊢\left(A\in ℂ\wedge x\in D\right)\to \log x\in ℂ$$
10	6 7	reccld	$$⊢x\in D\to \frac{1}{x}\in ℂ$$
11	10	adantl	$$⊢\left(A\in ℂ\wedge x\in D\right)\to \frac{1}{x}\in ℂ$$
12		mulcl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to Ay\in ℂ$$
13		efcl	$$⊢Ay\in ℂ\to {\mathrm{e}}^{Ay}\in ℂ$$
14	12 13	syl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to {\mathrm{e}}^{Ay}\in ℂ$$
15		ovexd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to {\mathrm{e}}^{Ay}A\in \mathrm{V}$$
16	1	logcn	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ$$
17		cncff	$$⊢\left({log\upharpoonright }_D\right):D\underset{cn}{⟶}ℂ\to \left({log\upharpoonright }_D\right):D⟶ℂ$$
18	16 17	mp1i	$$⊢A\in ℂ\to \left({log\upharpoonright }_D\right):D⟶ℂ$$
19	18	feqmptd	$$⊢A\in ℂ\to {log\upharpoonright }_D=\left(x\in D⟼\left({log\upharpoonright }_D\right)\left(x\right)\right)$$
20		fvres	$$⊢x\in D\to \left({log\upharpoonright }_D\right)\left(x\right)=\log x$$
21	20	mpteq2ia	$$⊢\left(x\in D⟼\left({log\upharpoonright }_D\right)\left(x\right)\right)=\left(x\in D⟼\log x\right)$$
22	19 21	eqtrdi	$$⊢A\in ℂ\to {log\upharpoonright }_D=\left(x\in D⟼\log x\right)$$
23	22	oveq2d	$$⊢A\in ℂ\to ℂ\mathrm{D}\left({log\upharpoonright }_D\right)=\frac{d\left(x\in D⟼\log x\right)}{d_{ℂ}x}$$
24	1	dvlog	$$⊢ℂ\mathrm{D}\left({log\upharpoonright }_D\right)=\left(x\in D⟼\frac{1}{x}\right)$$
25	23 24	eqtr3di	$$⊢A\in ℂ\to \frac{d\left(x\in D⟼\log x\right)}{d_{ℂ}x}=\left(x\in D⟼\frac{1}{x}\right)$$
26		simpl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to A\in ℂ$$
27		efcl	$$⊢x\in ℂ\to {\mathrm{e}}^x\in ℂ$$
28	27	adantl	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to {\mathrm{e}}^x\in ℂ$$
29		simpr	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to y\in ℂ$$
30		1cnd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to 1\in ℂ$$
31	3	dvmptid	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼y\right)}{d_{ℂ}y}=\left(y\in ℂ⟼1\right)$$
32		id	$$⊢A\in ℂ\to A\in ℂ$$
33	3 29 30 31 32	dvmptcmul	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼Ay\right)}{d_{ℂ}y}=\left(y\in ℂ⟼A\cdot 1\right)$$
34		mulid1	$$⊢A\in ℂ\to A\cdot 1=A$$
35	34	mpteq2dv	$$⊢A\in ℂ\to \left(y\in ℂ⟼A\cdot 1\right)=\left(y\in ℂ⟼A\right)$$
36	33 35	eqtrd	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼Ay\right)}{d_{ℂ}y}=\left(y\in ℂ⟼A\right)$$
37		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
38		eff	$$⊢\exp :ℂ⟶ℂ$$
39	38	a1i	$$⊢A\in ℂ\to \exp :ℂ⟶ℂ$$
40	39	feqmptd	$$⊢A\in ℂ\to \exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
41	40	oveq2d	$$⊢A\in ℂ\to ℂ\mathrm{D}\exp =\frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}$$
42	37 41 40	3eqtr3a	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
43		fveq2	$$⊢x=Ay\to {\mathrm{e}}^x={\mathrm{e}}^{Ay}$$
44	3 3 12 26 28 28 36 42 43 43	dvmptco	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼{\mathrm{e}}^{Ay}\right)}{d_{ℂ}y}=\left(y\in ℂ⟼{\mathrm{e}}^{Ay}A\right)$$
45		oveq2	$$⊢y=\log x\to Ay=A\log x$$
46	45	fveq2d	$$⊢y=\log x\to {\mathrm{e}}^{Ay}={\mathrm{e}}^{A\log x}$$
47	46	oveq1d	$$⊢y=\log x\to {\mathrm{e}}^{Ay}A={\mathrm{e}}^{A\log x}A$$
48	3 3 9 11 14 15 25 44 46 47	dvmptco	$$⊢A\in ℂ\to \frac{d\left(x\in D⟼{\mathrm{e}}^{A\log x}\right)}{d_{ℂ}x}=\left(x\in D⟼{\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)\right)$$
49	6	adantl	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x\in ℂ$$
50	7	adantl	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x\ne 0$$
51		simpl	$$⊢\left(A\in ℂ\wedge x\in D\right)\to A\in ℂ$$
52	49 50 51	cxpefd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^A={\mathrm{e}}^{A\log x}$$
53	52	mpteq2dva	$$⊢A\in ℂ\to \left(x\in D⟼x^A\right)=\left(x\in D⟼{\mathrm{e}}^{A\log x}\right)$$
54	53	oveq2d	$$⊢A\in ℂ\to \frac{d\left(x\in D⟼x^A\right)}{d_{ℂ}x}=\frac{d\left(x\in D⟼{\mathrm{e}}^{A\log x}\right)}{d_{ℂ}x}$$
55		1cnd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to 1\in ℂ$$
56	49 50 51 55	cxpsubd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^{A-1}=\frac{x^A}{x^1}$$
57	49	cxp1d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^1=x$$
58	57	oveq2d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to \frac{x^A}{x^1}=\frac{x^A}{x}$$
59	49 51	cxpcld	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^A\in ℂ$$
60	59 49 50	divrecd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to \frac{x^A}{x}=x^A\left(\frac{1}{x}\right)$$
61	56 58 60	3eqtrd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^{A-1}=x^A\left(\frac{1}{x}\right)$$
62	61	oveq2d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to A{x}^{A-1}=A{x}^A\left(\frac{1}{x}\right)$$
63	51 59 11	mul12d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to A{x}^A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
64	59 51 11	mulassd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^{A}A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
65	63 64	eqtr4d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to A{x}^A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
66	52	oveq1d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^{A}A={\mathrm{e}}^{A\log x}A$$
67	66	oveq1d	$$⊢\left(A\in ℂ\wedge x\in D\right)\to x^{A}A\left(\frac{1}{x}\right)={\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)$$
68	62 65 67	3eqtrd	$$⊢\left(A\in ℂ\wedge x\in D\right)\to A{x}^{A-1}={\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)$$
69	68	mpteq2dva	$$⊢A\in ℂ\to \left(x\in D⟼A{x}^{A-1}\right)=\left(x\in D⟼{\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)\right)$$
70	48 54 69	3eqtr4d	$$⊢A\in ℂ\to \frac{d\left(x\in D⟼x^A\right)}{d_{ℂ}x}=\left(x\in D⟼A{x}^{A-1}\right)$$