Theorem dvexp

Description: Derivative of a power function. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Assertion	dvexp	$$⊢N\in \mathbb{N}\to \frac{d\left(x\in ℂ⟼x^N\right)}{d_{ℂ}x}=\left(x\in ℂ⟼N{x}^{N-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=1\to x^n=x^1$$
2	1	mpteq2dv	$$⊢n=1\to \left(x\in ℂ⟼x^n\right)=\left(x\in ℂ⟼x^1\right)$$
3	2	oveq2d	$$⊢n=1\to \frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼x^1\right)}{d_{ℂ}x}$$
4		id	$$⊢n=1\to n=1$$
5		oveq1	$$⊢n=1\to n-1=1-1$$
6	5	oveq2d	$$⊢n=1\to x^{n-1}=x^{1-1}$$
7	4 6	oveq12d	$$⊢n=1\to n{x}^{n-1}=1x^{1-1}$$
8	7	mpteq2dv	$$⊢n=1\to \left(x\in ℂ⟼n{x}^{n-1}\right)=\left(x\in ℂ⟼1x^{1-1}\right)$$
9	3 8	eqeq12d	$$⊢n=1\to \left(\frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\left(x\in ℂ⟼n{x}^{n-1}\right)\leftrightarrow \frac{d\left(x\in ℂ⟼x^1\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1x^{1-1}\right)\right)$$
10		oveq2	$$⊢n=k\to x^n=x^k$$
11	10	mpteq2dv	$$⊢n=k\to \left(x\in ℂ⟼x^n\right)=\left(x\in ℂ⟼x^k\right)$$
12	11	oveq2d	$$⊢n=k\to \frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}$$
13		id	$$⊢n=k\to n=k$$
14		oveq1	$$⊢n=k\to n-1=k-1$$
15	14	oveq2d	$$⊢n=k\to x^{n-1}=x^{k-1}$$
16	13 15	oveq12d	$$⊢n=k\to n{x}^{n-1}=k{x}^{k-1}$$
17	16	mpteq2dv	$$⊢n=k\to \left(x\in ℂ⟼n{x}^{n-1}\right)=\left(x\in ℂ⟼k{x}^{k-1}\right)$$
18	12 17	eqeq12d	$$⊢n=k\to \left(\frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\left(x\in ℂ⟼n{x}^{n-1}\right)\leftrightarrow \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)$$
19		oveq2	$$⊢n=k+1\to x^n=x^{k+1}$$
20	19	mpteq2dv	$$⊢n=k+1\to \left(x\in ℂ⟼x^n\right)=\left(x\in ℂ⟼x^{k+1}\right)$$
21	20	oveq2d	$$⊢n=k+1\to \frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}$$
22		id	$$⊢n=k+1\to n=k+1$$
23		oveq1	$$⊢n=k+1\to n-1=k+1-1$$
24	23	oveq2d	$$⊢n=k+1\to x^{n-1}=x^{k+1-1}$$
25	22 24	oveq12d	$$⊢n=k+1\to n{x}^{n-1}=\left(k+1\right)x^{k+1-1}$$
26	25	mpteq2dv	$$⊢n=k+1\to \left(x\in ℂ⟼n{x}^{n-1}\right)=\left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)$$
27	21 26	eqeq12d	$$⊢n=k+1\to \left(\frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\left(x\in ℂ⟼n{x}^{n-1}\right)\leftrightarrow \frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)\right)$$
28		oveq2	$$⊢n=N\to x^n=x^N$$
29	28	mpteq2dv	$$⊢n=N\to \left(x\in ℂ⟼x^n\right)=\left(x\in ℂ⟼x^N\right)$$
30	29	oveq2d	$$⊢n=N\to \frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\frac{d\left(x\in ℂ⟼x^N\right)}{d_{ℂ}x}$$
31		id	$$⊢n=N\to n=N$$
32		oveq1	$$⊢n=N\to n-1=N-1$$
33	32	oveq2d	$$⊢n=N\to x^{n-1}=x^{N-1}$$
34	31 33	oveq12d	$$⊢n=N\to n{x}^{n-1}=N{x}^{N-1}$$
35	34	mpteq2dv	$$⊢n=N\to \left(x\in ℂ⟼n{x}^{n-1}\right)=\left(x\in ℂ⟼N{x}^{N-1}\right)$$
36	30 35	eqeq12d	$$⊢n=N\to \left(\frac{d\left(x\in ℂ⟼x^n\right)}{d_{ℂ}x}=\left(x\in ℂ⟼n{x}^{n-1}\right)\leftrightarrow \frac{d\left(x\in ℂ⟼x^N\right)}{d_{ℂ}x}=\left(x\in ℂ⟼N{x}^{N-1}\right)\right)$$
37		exp1	$$⊢x\in ℂ\to x^1=x$$
38	37	mpteq2ia	$$⊢\left(x\in ℂ⟼x^1\right)=\left(x\in ℂ⟼x\right)$$
39		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{ℂ}=\left(x\in ℂ⟼x\right)$$
40	38 39	eqtr4i	$$⊢\left(x\in ℂ⟼x^1\right)={\mathrm{I}\upharpoonright }_{ℂ}$$
41	40	oveq2i	$$⊢\frac{d\left(x\in ℂ⟼x^1\right)}{d_{ℂ}x}=ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)$$
42		1m1e0	$$⊢1-1=0$$
43	42	oveq2i	$$⊢x^{1-1}=x^0$$
44		exp0	$$⊢x\in ℂ\to x^0=1$$
45	43 44	eqtrid	$$⊢x\in ℂ\to x^{1-1}=1$$
46	45	oveq2d	$$⊢x\in ℂ\to 1x^{1-1}=1\cdot 1$$
47		1t1e1	$$⊢1\cdot 1=1$$
48	46 47	eqtrdi	$$⊢x\in ℂ\to 1x^{1-1}=1$$
49	48	mpteq2ia	$$⊢\left(x\in ℂ⟼1x^{1-1}\right)=\left(x\in ℂ⟼1\right)$$
50		fconstmpt	$$⊢ℂ\times \left\{1\right\}=\left(x\in ℂ⟼1\right)$$
51	49 50	eqtr4i	$$⊢\left(x\in ℂ⟼1x^{1-1}\right)=ℂ\times \left\{1\right\}$$
52		dvid	$$⊢ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=ℂ\times \left\{1\right\}$$
53	51 52	eqtr4i	$$⊢\left(x\in ℂ⟼1x^{1-1}\right)=ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)$$
54	41 53	eqtr4i	$$⊢\frac{d\left(x\in ℂ⟼x^1\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1x^{1-1}\right)$$
55		nncn	$$⊢k\in \mathbb{N}\to k\in ℂ$$
56	55	adantr	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k\in ℂ$$
57		ax-1cn	$$⊢1\in ℂ$$
58		pncan	$$⊢\left(k\in ℂ\wedge 1\in ℂ\right)\to k+1-1=k$$
59	56 57 58	sylancl	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k+1-1=k$$
60	59	oveq2d	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x^{k+1-1}=x^k$$
61	60	oveq2d	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to \left(k+1\right)x^{k+1-1}=\left(k+1\right)x^k$$
62	57	a1i	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to 1\in ℂ$$
63		id	$$⊢x\in ℂ\to x\in ℂ$$
64		nnnn0	$$⊢k\in \mathbb{N}\to k\in {\mathbb{N}}_0$$
65		expcl	$$⊢\left(x\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to x^k\in ℂ$$
66	63 64 65	syl2anr	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x^k\in ℂ$$
67	56 62 66	adddird	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to \left(k+1\right)x^k=k{x}^k+1x^k$$
68	66	mullidd	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to 1x^k=x^k$$
69	68	oveq2d	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^k+1x^k=k{x}^k+x^k$$
70	61 67 69	3eqtrd	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to \left(k+1\right)x^{k+1-1}=k{x}^k+x^k$$
71	70	mpteq2dva	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)=\left(x\in ℂ⟼k{x}^k+x^k\right)$$
72		cnex	$$⊢ℂ\in \mathrm{V}$$
73	72	a1i	$$⊢k\in \mathbb{N}\to ℂ\in \mathrm{V}$$
74	56 66	mulcld	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^k\in ℂ$$
75		nnm1nn0	$$⊢k\in \mathbb{N}\to k-1\in {\mathbb{N}}_0$$
76		expcl	$$⊢\left(x\in ℂ\wedge k-1\in {\mathbb{N}}_0\right)\to x^{k-1}\in ℂ$$
77	63 75 76	syl2anr	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x^{k-1}\in ℂ$$
78	56 77	mulcld	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^{k-1}\in ℂ$$
79		simpr	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x\in ℂ$$
80		eqidd	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼k{x}^{k-1}\right)=\left(x\in ℂ⟼k{x}^{k-1}\right)$$
81	39	a1i	$$⊢k\in \mathbb{N}\to {\mathrm{I}\upharpoonright }_{ℂ}=\left(x\in ℂ⟼x\right)$$
82	73 78 79 80 81	offval2	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼k{x}^{k-1}x\right)$$
83	56 77 79	mulassd	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^{k-1}x=k{x}^{k-1}x$$
84		expm1t	$$⊢\left(x\in ℂ\wedge k\in \mathbb{N}\right)\to x^k=x^{k-1}x$$
85	84	ancoms	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x^k=x^{k-1}x$$
86	85	oveq2d	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^k=k{x}^{k-1}x$$
87	83 86	eqtr4d	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to k{x}^{k-1}x=k{x}^k$$
88	87	mpteq2dva	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼k{x}^{k-1}x\right)=\left(x\in ℂ⟼k{x}^k\right)$$
89	82 88	eqtrd	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼k{x}^k\right)$$
90	52 50	eqtri	$$⊢ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼1\right)$$
91	90	a1i	$$⊢k\in \mathbb{N}\to ℂ\mathrm{D}\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼1\right)$$
92		eqidd	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼x^k\right)=\left(x\in ℂ⟼x^k\right)$$
93	73 62 66 91 92	offval2	$$⊢k\in \mathbb{N}\to {\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)=\left(x\in ℂ⟼1x^k\right)$$
94	68	mpteq2dva	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼1x^k\right)=\left(x\in ℂ⟼x^k\right)$$
95	93 94	eqtrd	$$⊢k\in \mathbb{N}\to {\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)=\left(x\in ℂ⟼x^k\right)$$
96	73 74 66 89 95	offval2	$$⊢k\in \mathbb{N}\to \left(\left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)=\left(x\in ℂ⟼k{x}^k+x^k\right)$$
97	71 96	eqtr4d	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)=\left(\left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)$$
98		oveq1	$$⊢\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\to \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}{\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)$$
99	98	oveq1d	$$⊢\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\to \left(\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}{\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)=\left(\left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)$$
100	99	eqcomd	$$⊢\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\to \left(\left(x\in ℂ⟼k{x}^{k-1}\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)=\left(\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}{\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)$$
101	97 100	sylan9eq	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)=\left(\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}{\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)$$
102		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
103	102	a1i	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to ℂ\in \left\{ℝ,ℂ\right\}$$
104	66	fmpttd	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼x^k\right):ℂ⟶ℂ$$
105	104	adantr	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \left(x\in ℂ⟼x^k\right):ℂ⟶ℂ$$
106		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{ℂ}\right):ℂ\underset{1-1\; onto}{⟶}ℂ$$
107		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_{ℂ}\right):ℂ\underset{1-1\; onto}{⟶}ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right):ℂ⟶ℂ$$
108	106 107	mp1i	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right):ℂ⟶ℂ$$
109		simpr	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)$$
110	109	dmeqd	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \mathrm{dom}\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\mathrm{dom}\left(x\in ℂ⟼k{x}^{k-1}\right)$$
111	78	fmpttd	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼k{x}^{k-1}\right):ℂ⟶ℂ$$
112	111	adantr	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \left(x\in ℂ⟼k{x}^{k-1}\right):ℂ⟶ℂ$$
113	112	fdmd	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \mathrm{dom}\left(x\in ℂ⟼k{x}^{k-1}\right)=ℂ$$
114	110 113	eqtrd	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \mathrm{dom}\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=ℂ$$
115		1ex	$$⊢1\in \mathrm{V}$$
116	115	fconst	$$⊢\left(ℂ\times \left\{1\right\}\right):ℂ⟶\left\{1\right\}$$
117	52	feq1i	$$⊢{\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }:ℂ⟶\left\{1\right\}\leftrightarrow \left(ℂ\times \left\{1\right\}\right):ℂ⟶\left\{1\right\}$$
118	116 117	mpbir	$$⊢{\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }:ℂ⟶\left\{1\right\}$$
119	118	fdmi	$$⊢\mathrm{dom}{\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }=ℂ$$
120	119	a1i	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \mathrm{dom}{\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }=ℂ$$
121	103 105 108 114 120	dvmulf	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to ℂ\mathrm{D}\left(\left(x\in ℂ⟼x^k\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right)=\left(\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}{\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right){+}_f\left({\left({\mathrm{I}\upharpoonright }_{ℂ}\right)}_{ℂ}^{\prime }{\times }_f\left(x\in ℂ⟼x^k\right)\right)$$
122	73 66 79 92 81	offval2	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼x^k\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼x^{k}x\right)$$
123		expp1	$$⊢\left(x\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to x^{k+1}=x^{k}x$$
124	63 64 123	syl2anr	$$⊢\left(k\in \mathbb{N}\wedge x\in ℂ\right)\to x^{k+1}=x^{k}x$$
125	124	mpteq2dva	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼x^{k+1}\right)=\left(x\in ℂ⟼x^{k}x\right)$$
126	122 125	eqtr4d	$$⊢k\in \mathbb{N}\to \left(x\in ℂ⟼x^k\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)=\left(x\in ℂ⟼x^{k+1}\right)$$
127	126	oveq2d	$$⊢k\in \mathbb{N}\to ℂ\mathrm{D}\left(\left(x\in ℂ⟼x^k\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right)=\frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}$$
128	127	adantr	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to ℂ\mathrm{D}\left(\left(x\in ℂ⟼x^k\right){\times }_f\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\right)=\frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}$$
129	101 121 128	3eqtr2rd	$$⊢\left(k\in \mathbb{N}\wedge \frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\right)\to \frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)$$
130	129	ex	$$⊢k\in \mathbb{N}\to \left(\frac{d\left(x\in ℂ⟼x^k\right)}{d_{ℂ}x}=\left(x\in ℂ⟼k{x}^{k-1}\right)\to \frac{d\left(x\in ℂ⟼x^{k+1}\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\left(k+1\right)x^{k+1-1}\right)\right)$$
131	9 18 27 36 54 130	nnind	$$⊢N\in \mathbb{N}\to \frac{d\left(x\in ℂ⟼x^N\right)}{d_{ℂ}x}=\left(x\in ℂ⟼N{x}^{N-1}\right)$$