---

Step * 1 1 1 1 1 of Lemma rpoly-nth-deriv-linear


1. x : ℝ
2. v : ℝ
3. v1 : ℝ
4. v2 : ℝ
5. m : ℕ
⊢ ((v * (v1 + v2)/r((m)!)) * x^m) = (((v * v1/r((m)!)) * x^m) + ((v * v2/r((m)!)) * x^m))
BY
{ (nRMul ⌜r((m)!)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  v  :  \mBbbR{}
3.  v1  :  \mBbbR{}
4.  v2  :  \mBbbR{}
5.  m  :  \mBbbN{}
\mvdash{}  ((v  *  (v1  +  v2)/r((m)!))  *  x\^{}m)  =  (((v  *  v1/r((m)!))  *  x\^{}m)  +  ((v  *  v2/r((m)!))  *  x\^{}m))


By

---

Latex:
(nRMul  \mkleeneopen{}r((m)!)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index