---

Step * of Lemma rpolydiv-property

No Annotations
∀[n:ℕ+]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[z,x:ℝ].
  ((Σi≤n. a_i * x^i) = (((x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i)) + (Σi≤n. a_i * z^i)))
BY
{ (Intros
   THEN (Unhide THENA Auto)
   THEN (Assert ((x - z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i))
               = ((x * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i)) + (-(z) * (Σi≤n - 1. rpolydiv(n;a;z)_i * x^i))) BY
               Auto)
   THEN ((RWO  "-1" 0 THENA Auto) THEN Thin (-1))
   THEN (RWO  "shift-rpolynomial" 0 THENA Auto)
   THEN (RWO  "rmul-rpolynomial" 0 THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n 0 THENA Auto)
   THEN Unfold `rpolynomial` 0
   THEN Reduce 0
   THEN (RW (AddrC [2;1;1] (LemmaC `rsum-split-last`)) 0 THENA Auto)
   THEN (Subst' (n =z 0) ~ ff 0 THENA Auto)
   THEN Reduce 0
   THEN (RW (AddrC [1] (LemmaC `rsum-split-last`)) 0 THENA Auto)) }

1
1. n : ℕ+
2. a : ℕn + 1 ⟶ ℝ
3. z : ℝ
4. x : ℝ
⊢ (Σ{(a i) * x^i | 0≤i≤n - 1} + ((a n) * x^n))
= (((Σ{if (i =z 0) then r0 else rpolydiv(n;a;z) (i - 1) fi  * x^i | 0≤i≤n - 1} + ((rpolydiv(n;a;z) (n - 1)) * x^n))
  + Σ{(-(z) * (rpolydiv(n;a;z) i)) * x^i | 0≤i≤n - 1})
  + Σ{(a i) * z^i | 0≤i≤n})

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[z,x:\mBbbR{}].
    ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  =  (((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i))  +  (\mSigma{}i\mleq{}n.  a\_i  *  z\^{}i)))


By

---

Latex:
(Intros
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  ((x  -  z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i))
                          =  ((x  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i))
                              +  (-(z)  *  (\mSigma{}i\mleq{}n  -  1.  rpolydiv(n;a;z)\_i  *  x\^{}i)))  BY
                          Auto)
  THEN  ((RWO    "-1"  0  THENA  Auto)  THEN  Thin  (-1))
  THEN  (RWO    "shift-rpolynomial"  0  THENA  Auto)
  THEN  (RWO    "rmul-rpolynomial"  0  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto)
  THEN  Unfold  `rpolynomial`  0
  THEN  Reduce  0
  THEN  (RW  (AddrC  [2;1;1]  (LemmaC  `rsum-split-last`))  0  THENA  Auto)
  THEN  (Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RW  (AddrC  [1]  (LemmaC  `rsum-split-last`))  0  THENA  Auto))

---

Home Index