Metamath Proof Explorer


Theorem dvxpaek

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

Ref Expression
Hypotheses dvxpaek.s φ S
dvxpaek.x φ X TopOpen fld 𝑡 S
dvxpaek.a φ A
dvxpaek.k φ K
Assertion dvxpaek φ dx X x + A K dS x = x X K x + A K 1

Proof

Step Hyp Ref Expression
1 dvxpaek.s φ S
2 dvxpaek.x φ X TopOpen fld 𝑡 S
3 dvxpaek.a φ A
4 dvxpaek.k φ K
5 cnelprrecn
6 5 a1i φ
7 1 2 dvdmsscn φ X
8 7 adantr φ x X X
9 simpr φ x X x X
10 8 9 sseldd φ x X x
11 3 adantr φ x X A
12 10 11 addcld φ x X x + A
13 1red φ x X 1
14 0red φ x X 0
15 13 14 readdcld φ x X 1 + 0
16 simpr φ y y
17 4 nnnn0d φ K 0
18 17 adantr φ y K 0
19 16 18 expcld φ y y K
20 18 nn0cnd φ y K
21 nnm1nn0 K K 1 0
22 4 21 syl φ K 1 0
23 22 adantr φ y K 1 0
24 16 23 expcld φ y y K 1
25 20 24 mulcld φ y K y K 1
26 1 2 dvmptidg φ dx X x dS x = x X 1
27 1 2 3 dvmptconst φ dx X A dS x = x X 0
28 1 10 13 26 11 14 27 dvmptadd φ dx X x + A dS x = x X 1 + 0
29 dvexp K dy y K d y = y K y K 1
30 4 29 syl φ dy y K d y = y K 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 y K 1 = K x + A K 1
34 1 6 12 15 19 25 28 30 31 33 dvmptco φ dx X x + A K dS x = x X K x + A K 1 1 + 0
35 1p0e1 1 + 0 = 1
36 35 oveq2i K x + A K 1 1 + 0 = K x + A K 1 1
37 36 a1i φ x X K x + A K 1 1 + 0 = K x + A K 1 1
38 4 nncnd φ K
39 38 adantr φ x X K
40 22 adantr φ x X K 1 0
41 12 40 expcld φ x X x + A K 1
42 39 41 mulcld φ x X K x + A K 1
43 42 mulid1d φ x X K x + A K 1 1 = K x + A K 1
44 37 43 eqtrd φ x X K x + A K 1 1 + 0 = K x + A K 1
45 44 mpteq2dva φ x X K x + A K 1 1 + 0 = x X K x + A K 1
46 34 45 eqtrd φ dx X x + A K dS x = x X K x + A K 1