---

Step * of Lemma rdiv-rpolynomial

∀[n:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[x,b:ℝ].  ((Σi≤n. a_i * x^i)/b) = (Σi≤n. λi.(a i/b)_i * x^i) supposing b ≠ r0
BY
{ ((Auto THEN Unfold `rdiv` 0) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  Unfold  `rdiv`  0)  THEN  Auto)

---

Home Index