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

Proof

Step	Hyp	Ref	Expression
1		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
2	1	a1i	$$⊢A\in ℂ\to ℝ\in \left\{ℝ,ℂ\right\}$$
3		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
4	3	adantl	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \log x\in ℝ$$
5		rpreccl	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in {ℝ}^{+}$$
6	5	adantl	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in {ℝ}^{+}$$
7		recn	$$⊢y\in ℝ\to y\in ℂ$$
8		mulcl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to Ay\in ℂ$$
9		efcl	$$⊢Ay\in ℂ\to {\mathrm{e}}^{Ay}\in ℂ$$
10	8 9	syl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to {\mathrm{e}}^{Ay}\in ℂ$$
11	7 10	sylan2	$$⊢\left(A\in ℂ\wedge y\in ℝ\right)\to {\mathrm{e}}^{Ay}\in ℂ$$
12		ovexd	$$⊢\left(A\in ℂ\wedge y\in ℝ\right)\to {\mathrm{e}}^{Ay}A\in \mathrm{V}$$
13		relogf1o	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
14		f1of	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
15	13 14	mp1i	$$⊢A\in ℂ\to \left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}⟶ℝ$$
16	15	feqmptd	$$⊢A\in ℂ\to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)$$
17		fvres	$$⊢x\in {ℝ}^{+}\to \left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)=\log x$$
18	17	mpteq2ia	$$⊢\left(x\in {ℝ}^{+}⟼\left({log\upharpoonright }_{{ℝ}^{+}}\right)\left(x\right)\right)=\left(x\in {ℝ}^{+}⟼\log x\right)$$
19	16 18	eqtrdi	$$⊢A\in ℂ\to {log\upharpoonright }_{{ℝ}^{+}}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
20	19	oveq2d	$$⊢A\in ℂ\to ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}$$
21		dvrelog	$$⊢ℝ\mathrm{D}\left({log\upharpoonright }_{{ℝ}^{+}}\right)=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
22	20 21	eqtr3di	$$⊢A\in ℂ\to \frac{d\left(x\in {ℝ}^{+}⟼\log x\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\frac{1}{x}\right)$$
23		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
24	23	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
25		toponmax	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
26	24 25	mp1i	$$⊢A\in ℂ\to ℂ\in \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
27		ax-resscn	$$⊢ℝ\subseteq ℂ$$
28	27	a1i	$$⊢A\in ℂ\to ℝ\subseteq ℂ$$
29		df-ss	$$⊢ℝ\subseteq ℂ\leftrightarrow ℝ\cap ℂ=ℝ$$
30	28 29	sylib	$$⊢A\in ℂ\to ℝ\cap ℂ=ℝ$$
31		ovexd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to {\mathrm{e}}^{Ay}A\in \mathrm{V}$$
32		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
33	32	a1i	$$⊢A\in ℂ\to ℂ\in \left\{ℝ,ℂ\right\}$$
34		simpl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to A\in ℂ$$
35		efcl	$$⊢x\in ℂ\to {\mathrm{e}}^x\in ℂ$$
36	35	adantl	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to {\mathrm{e}}^x\in ℂ$$
37		simpr	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to y\in ℂ$$
38		1cnd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to 1\in ℂ$$
39	33	dvmptid	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼y\right)}{d_{ℂ}y}=\left(y\in ℂ⟼1\right)$$
40		id	$$⊢A\in ℂ\to A\in ℂ$$
41	33 37 38 39 40	dvmptcmul	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼Ay\right)}{d_{ℂ}y}=\left(y\in ℂ⟼A\cdot 1\right)$$
42		mulrid	$$⊢A\in ℂ\to A\cdot 1=A$$
43	42	mpteq2dv	$$⊢A\in ℂ\to \left(y\in ℂ⟼A\cdot 1\right)=\left(y\in ℂ⟼A\right)$$
44	41 43	eqtrd	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼Ay\right)}{d_{ℂ}y}=\left(y\in ℂ⟼A\right)$$
45		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
46		eff	$$⊢\exp :ℂ⟶ℂ$$
47	46	a1i	$$⊢A\in ℂ\to \exp :ℂ⟶ℂ$$
48	47	feqmptd	$$⊢A\in ℂ\to \exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
49	48	eqcomd	$$⊢A\in ℂ\to \left(x\in ℂ⟼{\mathrm{e}}^x\right)=\exp$$
50	49	oveq2d	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}=ℂ\mathrm{D}\exp$$
51	45 50 49	3eqtr4a	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼{\mathrm{e}}^x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
52		fveq2	$$⊢x=Ay\to {\mathrm{e}}^x={\mathrm{e}}^{Ay}$$
53	33 33 8 34 36 36 44 51 52 52	dvmptco	$$⊢A\in ℂ\to \frac{d\left(y\in ℂ⟼{\mathrm{e}}^{Ay}\right)}{d_{ℂ}y}=\left(y\in ℂ⟼{\mathrm{e}}^{Ay}A\right)$$
54	23 2 26 30 10 31 53	dvmptres3	$$⊢A\in ℂ\to \frac{d\left(y\in ℝ⟼{\mathrm{e}}^{Ay}\right)}{d_{ℝ}y}=\left(y\in ℝ⟼{\mathrm{e}}^{Ay}A\right)$$
55		oveq2	$$⊢y=\log x\to Ay=A\log x$$
56	55	fveq2d	$$⊢y=\log x\to {\mathrm{e}}^{Ay}={\mathrm{e}}^{A\log x}$$
57	56	oveq1d	$$⊢y=\log x\to {\mathrm{e}}^{Ay}A={\mathrm{e}}^{A\log x}A$$
58	2 2 4 6 11 12 22 54 56 57	dvmptco	$$⊢A\in ℂ\to \frac{d\left(x\in {ℝ}^{+}⟼{\mathrm{e}}^{A\log x}\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼{\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)\right)$$
59		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
60	59	adantl	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x\in ℂ$$
61		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
62	61	adantl	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x\ne 0$$
63		simpl	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to A\in ℂ$$
64	60 62 63	cxpefd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^A={\mathrm{e}}^{A\log x}$$
65	64	mpteq2dva	$$⊢A\in ℂ\to \left(x\in {ℝ}^{+}⟼x^A\right)=\left(x\in {ℝ}^{+}⟼{\mathrm{e}}^{A\log x}\right)$$
66	65	oveq2d	$$⊢A\in ℂ\to \frac{d\left(x\in {ℝ}^{+}⟼x^A\right)}{d_{ℝ}x}=\frac{d\left(x\in {ℝ}^{+}⟼{\mathrm{e}}^{A\log x}\right)}{d_{ℝ}x}$$
67		1cnd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to 1\in ℂ$$
68	60 62 63 67	cxpsubd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^{A-1}=\frac{x^A}{x^1}$$
69	60	cxp1d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^1=x$$
70	69	oveq2d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \frac{x^A}{x^1}=\frac{x^A}{x}$$
71	60 63	cxpcld	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^A\in ℂ$$
72	71 60 62	divrecd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \frac{x^A}{x}=x^A\left(\frac{1}{x}\right)$$
73	68 70 72	3eqtrd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^{A-1}=x^A\left(\frac{1}{x}\right)$$
74	73	oveq2d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to A{x}^{A-1}=A{x}^A\left(\frac{1}{x}\right)$$
75	6	rpcnd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \frac{1}{x}\in ℂ$$
76	63 71 75	mul12d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to A{x}^A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
77	71 63 75	mulassd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^{A}A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
78	76 77	eqtr4d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to A{x}^A\left(\frac{1}{x}\right)=x^{A}A\left(\frac{1}{x}\right)$$
79	64	oveq1d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^{A}A={\mathrm{e}}^{A\log x}A$$
80	79	oveq1d	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to x^{A}A\left(\frac{1}{x}\right)={\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)$$
81	74 78 80	3eqtrd	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to A{x}^{A-1}={\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)$$
82	81	mpteq2dva	$$⊢A\in ℂ\to \left(x\in {ℝ}^{+}⟼A{x}^{A-1}\right)=\left(x\in {ℝ}^{+}⟼{\mathrm{e}}^{A\log x}A\left(\frac{1}{x}\right)\right)$$
83	58 66 82	3eqtr4d	$$⊢A\in ℂ\to \frac{d\left(x\in {ℝ}^{+}⟼x^A\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼A{x}^{A-1}\right)$$