dvxpaek

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

	Ref	Expression
Hypotheses	dvxpaek.s	\|- ( ph -> S e. { RR , CC } )
	dvxpaek.x	\|- ( ph -> X e. ( ( TopOpen ` CCfld ) \|`t S ) )
	dvxpaek.a	\|- ( ph -> A e. CC )
	dvxpaek.k	\|- ( ph -> K e. NN )
Assertion	dvxpaek	\|- ( ph -> ( S _D ( x e. X \|-> ( ( x + A ) ^ K ) ) ) = ( x e. X \|-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvxpaek.s	\|- ( ph -> S e. { RR , CC } )
2		dvxpaek.x	\|- ( ph -> X e. ( ( TopOpen ` CCfld ) \|`t S ) )
3		dvxpaek.a	\|- ( ph -> A e. CC )
4		dvxpaek.k	\|- ( ph -> K e. NN )
5		cnelprrecn	\|- CC e. { RR , CC }
6	5	a1i	\|- ( ph -> CC e. { RR , CC } )
7	1 2	dvdmsscn	\|- ( ph -> X C_ CC )
8	7	adantr	\|- ( ( ph /\ x e. X ) -> X C_ CC )
9		simpr	\|- ( ( ph /\ x e. X ) -> x e. X )
10	8 9	sseldd	\|- ( ( ph /\ x e. X ) -> x e. CC )
11	3	adantr	\|- ( ( ph /\ x e. X ) -> A e. CC )
12	10 11	addcld	\|- ( ( ph /\ x e. X ) -> ( x + A ) e. CC )
13		1red	\|- ( ( ph /\ x e. X ) -> 1 e. RR )
14		0red	\|- ( ( ph /\ x e. X ) -> 0 e. RR )
15	13 14	readdcld	\|- ( ( ph /\ x e. X ) -> ( 1 + 0 ) e. RR )
16		simpr	\|- ( ( ph /\ y e. CC ) -> y e. CC )
17	4	nnnn0d	\|- ( ph -> K e. NN0 )
18	17	adantr	\|- ( ( ph /\ y e. CC ) -> K e. NN0 )
19	16 18	expcld	\|- ( ( ph /\ y e. CC ) -> ( y ^ K ) e. CC )
20	18	nn0cnd	\|- ( ( ph /\ y e. CC ) -> K e. CC )
21		nnm1nn0	\|- ( K e. NN -> ( K - 1 ) e. NN0 )
22	4 21	syl	\|- ( ph -> ( K - 1 ) e. NN0 )
23	22	adantr	\|- ( ( ph /\ y e. CC ) -> ( K - 1 ) e. NN0 )
24	16 23	expcld	\|- ( ( ph /\ y e. CC ) -> ( y ^ ( K - 1 ) ) e. CC )
25	20 24	mulcld	\|- ( ( ph /\ y e. CC ) -> ( K x. ( y ^ ( K - 1 ) ) ) e. CC )
26	1 2	dvmptidg	\|- ( ph -> ( S _D ( x e. X \|-> x ) ) = ( x e. X \|-> 1 ) )
27	1 2 3	dvmptconst	\|- ( ph -> ( S _D ( x e. X \|-> A ) ) = ( x e. X \|-> 0 ) )
28	1 10 13 26 11 14 27	dvmptadd	\|- ( ph -> ( S _D ( x e. X \|-> ( x + A ) ) ) = ( x e. X \|-> ( 1 + 0 ) ) )
29		dvexp	\|- ( K e. NN -> ( CC _D ( y e. CC \|-> ( y ^ K ) ) ) = ( y e. CC \|-> ( K x. ( y ^ ( K - 1 ) ) ) ) )
30	4 29	syl	\|- ( ph -> ( CC _D ( y e. CC \|-> ( y ^ K ) ) ) = ( y e. CC \|-> ( K x. ( y ^ ( K - 1 ) ) ) ) )
31		oveq1	\|- ( y = ( x + A ) -> ( y ^ K ) = ( ( x + A ) ^ K ) )
32		oveq1	\|- ( y = ( x + A ) -> ( y ^ ( K - 1 ) ) = ( ( x + A ) ^ ( K - 1 ) ) )
33	32	oveq2d	\|- ( y = ( x + A ) -> ( K x. ( y ^ ( K - 1 ) ) ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
34	1 6 12 15 19 25 28 30 31 33	dvmptco	\|- ( ph -> ( S _D ( x e. X \|-> ( ( x + A ) ^ K ) ) ) = ( x e. X \|-> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) ) )
35		1p0e1	\|- ( 1 + 0 ) = 1
36	35	oveq2i	\|- ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 )
37	36	a1i	\|- ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 ) )
38	4	nncnd	\|- ( ph -> K e. CC )
39	38	adantr	\|- ( ( ph /\ x e. X ) -> K e. CC )
40	22	adantr	\|- ( ( ph /\ x e. X ) -> ( K - 1 ) e. NN0 )
41	12 40	expcld	\|- ( ( ph /\ x e. X ) -> ( ( x + A ) ^ ( K - 1 ) ) e. CC )
42	39 41	mulcld	\|- ( ( ph /\ x e. X ) -> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) e. CC )
43	42	mulridd	\|- ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. 1 ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
44	37 43	eqtrd	\|- ( ( ph /\ x e. X ) -> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) = ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) )
45	44	mpteq2dva	\|- ( ph -> ( x e. X \|-> ( ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) x. ( 1 + 0 ) ) ) = ( x e. X \|-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )
46	34 45	eqtrd	\|- ( ph -> ( S _D ( x e. X \|-> ( ( x + A ) ^ K ) ) ) = ( x e. X \|-> ( K x. ( ( x + A ) ^ ( K - 1 ) ) ) ) )

Metamath Proof Explorer

Theorem dvxpaek

Proof