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 ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvxpaek.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
dvxpaek.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
dvxpaek.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
Assertion dvxpaek ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dvxpaek.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvxpaek.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 dvxpaek.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 dvxpaek.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
5 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
6 5 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
7 1 2 dvdmsscn ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ⊆ ℂ )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
10 8 9 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ℂ )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
12 10 11 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 + 𝐴 ) ∈ ℂ )
13 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ )
14 0red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℝ )
15 13 14 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 1 + 0 ) ∈ ℝ )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
17 4 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐾 ∈ ℕ0 )
19 16 18 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝐾 ) ∈ ℂ )
20 18 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐾 ∈ ℂ )
21 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
22 4 21 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐾 − 1 ) ∈ ℕ0 )
24 16 23 expcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
25 20 24 mulcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐾 · ( 𝑦 ↑ ( 𝐾 − 1 ) ) ) ∈ ℂ )
26 1 2 dvmptidg ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ 1 ) )
27 1 2 3 dvmptconst ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
28 1 10 13 26 11 14 27 dvmptadd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝑥 + 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 1 + 0 ) ) )
29 dvexp ⊢ ( 𝐾 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝐾 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐾 · ( 𝑦 ↑ ( 𝐾 − 1 ) ) ) ) )
30 4 29 syl ⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝐾 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐾 · ( 𝑦 ↑ ( 𝐾 − 1 ) ) ) ) )
31 oveq1 ⊢ ( 𝑦 = ( 𝑥 + 𝐴 ) → ( 𝑦 ↑ 𝐾 ) = ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) )
32 oveq1 ⊢ ( 𝑦 = ( 𝑥 + 𝐴 ) → ( 𝑦 ↑ ( 𝐾 − 1 ) ) = ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) )
33 32 oveq2d ⊢ ( 𝑦 = ( 𝑥 + 𝐴 ) → ( 𝐾 · ( 𝑦 ↑ ( 𝐾 − 1 ) ) ) = ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) )
34 1 6 12 15 19 25 28 30 31 33 dvmptco ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · ( 1 + 0 ) ) ) )
35 1p0e1 ⊢ ( 1 + 0 ) = 1
36 35 oveq2i ⊢ ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · ( 1 + 0 ) ) = ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · 1 )
37 36 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · ( 1 + 0 ) ) = ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · 1 ) )
38 4 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ℂ )
40 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 − 1 ) ∈ ℕ0 )
41 12 40 expcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ∈ ℂ )
42 39 41 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) ∈ ℂ )
43 42 mulridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · 1 ) = ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) )
44 37 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · ( 1 + 0 ) ) = ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) )
45 44 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) · ( 1 + 0 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) ) )
46 34 45 eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 + 𝐴 ) ↑ 𝐾 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐾 · ( ( 𝑥 + 𝐴 ) ↑ ( 𝐾 − 1 ) ) ) ) )