Theorem dvxpaek

Description: Derivative of the polynomial ( x + A ) ^ K . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvxpaek.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvxpaek.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
	dvxpaek.a	$$⊢\phi \to A\in ℂ$$
	dvxpaek.k	$$⊢\phi \to K\in \mathbb{N}$$
Assertion	dvxpaek	$$⊢\phi \to \frac{d\left(x\in X⟼{\left(x+A\right)}^K\right)}{d_{S}x}=\left(x\in X⟼K{\left(x+A\right)}^{K-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvxpaek.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
2		dvxpaek.x	$$⊢\phi \to X\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)$$
3		dvxpaek.a	$$⊢\phi \to A\in ℂ$$
4		dvxpaek.k	$$⊢\phi \to K\in \mathbb{N}$$
5		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
6	5	a1i	$$⊢\phi \to ℂ\in \left\{ℝ,ℂ\right\}$$
7	1 2	dvdmsscn	$$⊢\phi \to X\subseteq ℂ$$
8	7	adantr	$$⊢\left(\phi \wedge x\in X\right)\to X\subseteq ℂ$$
9		simpr	$$⊢\left(\phi \wedge x\in X\right)\to x\in X$$
10	8 9	sseldd	$$⊢\left(\phi \wedge x\in X\right)\to x\in ℂ$$
11	3	adantr	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
12	10 11	addcld	$$⊢\left(\phi \wedge x\in X\right)\to x+A\in ℂ$$
13		1red	$$⊢\left(\phi \wedge x\in X\right)\to 1\in ℝ$$
14		0red	$$⊢\left(\phi \wedge x\in X\right)\to 0\in ℝ$$
15	13 14	readdcld	$$⊢\left(\phi \wedge x\in X\right)\to 1+0\in ℝ$$
16		simpr	$$⊢\left(\phi \wedge y\in ℂ\right)\to y\in ℂ$$
17	4	nnnn0d	$$⊢\phi \to K\in {\mathbb{N}}_0$$
18	17	adantr	$$⊢\left(\phi \wedge y\in ℂ\right)\to K\in {\mathbb{N}}_0$$
19	16 18	expcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to y^K\in ℂ$$
20	18	nn0cnd	$$⊢\left(\phi \wedge y\in ℂ\right)\to K\in ℂ$$
21		nnm1nn0	$$⊢K\in \mathbb{N}\to K-1\in {\mathbb{N}}_0$$
22	4 21	syl	$$⊢\phi \to K-1\in {\mathbb{N}}_0$$
23	22	adantr	$$⊢\left(\phi \wedge y\in ℂ\right)\to K-1\in {\mathbb{N}}_0$$
24	16 23	expcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to y^{K-1}\in ℂ$$
25	20 24	mulcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to K{y}^{K-1}\in ℂ$$
26	1 2	dvmptidg	$$⊢\phi \to \frac{d\left(x\in X⟼x\right)}{d_{S}x}=\left(x\in X⟼1\right)$$
27	1 2 3	dvmptconst	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼0\right)$$
28	1 10 13 26 11 14 27	dvmptadd	$$⊢\phi \to \frac{d\left(x\in X⟼x+A\right)}{d_{S}x}=\left(x\in X⟼1+0\right)$$
29		dvexp	$$⊢K\in \mathbb{N}\to \frac{d\left(y\in ℂ⟼y^K\right)}{d_{ℂ}y}=\left(y\in ℂ⟼K{y}^{K-1}\right)$$
30	4 29	syl	$$⊢\phi \to \frac{d\left(y\in ℂ⟼y^K\right)}{d_{ℂ}y}=\left(y\in ℂ⟼K{y}^{K-1}\right)$$
31		oveq1	$$⊢y=x+A\to y^K={\left(x+A\right)}^K$$
32		oveq1	$$⊢y=x+A\to y^{K-1}={\left(x+A\right)}^{K-1}$$
33	32	oveq2d	$$⊢y=x+A\to K{y}^{K-1}=K{\left(x+A\right)}^{K-1}$$
34	1 6 12 15 19 25 28 30 31 33	dvmptco	$$⊢\phi \to \frac{d\left(x\in X⟼{\left(x+A\right)}^K\right)}{d_{S}x}=\left(x\in X⟼K{\left(x+A\right)}^{K-1}\left(1+0\right)\right)$$
35		1p0e1	$$⊢1+0=1$$
36	35	oveq2i	$$⊢K{\left(x+A\right)}^{K-1}\left(1+0\right)=K{\left(x+A\right)}^{K-1}\cdot 1$$
37	36	a1i	$$⊢\left(\phi \wedge x\in X\right)\to K{\left(x+A\right)}^{K-1}\left(1+0\right)=K{\left(x+A\right)}^{K-1}\cdot 1$$
38	4	nncnd	$$⊢\phi \to K\in ℂ$$
39	38	adantr	$$⊢\left(\phi \wedge x\in X\right)\to K\in ℂ$$
40	22	adantr	$$⊢\left(\phi \wedge x\in X\right)\to K-1\in {\mathbb{N}}_0$$
41	12 40	expcld	$$⊢\left(\phi \wedge x\in X\right)\to {\left(x+A\right)}^{K-1}\in ℂ$$
42	39 41	mulcld	$$⊢\left(\phi \wedge x\in X\right)\to K{\left(x+A\right)}^{K-1}\in ℂ$$
43	42	mulid1d	$$⊢\left(\phi \wedge x\in X\right)\to K{\left(x+A\right)}^{K-1}\cdot 1=K{\left(x+A\right)}^{K-1}$$
44	37 43	eqtrd	$$⊢\left(\phi \wedge x\in X\right)\to K{\left(x+A\right)}^{K-1}\left(1+0\right)=K{\left(x+A\right)}^{K-1}$$
45	44	mpteq2dva	$$⊢\phi \to \left(x\in X⟼K{\left(x+A\right)}^{K-1}\left(1+0\right)\right)=\left(x\in X⟼K{\left(x+A\right)}^{K-1}\right)$$
46	34 45	eqtrd	$$⊢\phi \to \frac{d\left(x\in X⟼{\left(x+A\right)}^K\right)}{d_{S}x}=\left(x\in X⟼K{\left(x+A\right)}^{K-1}\right)$$