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	⊢ ( 𝜑 → 𝐾 ∈ ℕ₀ )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐾 ∈ ℕ₀ )
19	16 18	expcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝐾 ) ∈ ℂ )
20	18	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝐾 ∈ ℂ )
21		nnm1nn0	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ₀ )
22	4 21	syl	⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ₀ )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝐾 − 1 ) ∈ ℕ₀ )
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 ) ∈ ℕ₀ )
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 ) ) ) ) )

Metamath Proof Explorer

Theorem dvxpaek

Proof