---

Step * of Lemma subtract-rpolynomials-same-degree

∀[n:ℕ]. ∀[a,b:ℕn + 1 ⟶ ℝ]. ∀[x:ℝ].  (((Σi≤n. a_i * x^i) - (Σi≤n. b_i * x^i)) = (Σi≤n. λi.((a i) - b i)_i * x^i))
BY
{ (Auto
   THEN (RWO "subtract-rpolynomials" 0 THENA Auto)
   THEN BLemma `rpolynomial_functionality`
   THEN Auto
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    (((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  -  (\mSigma{}i\mleq{}n.  b\_i  *  x\^{}i))  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  -  b  i)\_i  *  x\^{}i))


By

---

Latex:
(Auto
  THEN  (RWO  "subtract-rpolynomials"  0  THENA  Auto)
  THEN  BLemma  `rpolynomial\_functionality`
  THEN  Auto
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto)

---

Home Index