---

Step * 1 of Lemma rpolydiv-property


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})
BY
{ ((Subst' rpolydiv(n;a;z) (n - 1) ~ a n 0
    THENA ((Unfold `rpolydiv` 0 THEN Reduce 0) THEN (Subst' n - 1 - n - 1 ~ 0 0 THENA Auto) THEN Reduce 0 THEN Auto)
    )
   THEN (nRAdd ⌜-((a n) * x^n)⌝ 0⋅ THENA Auto)
   ) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  z  :  \mBbbR{}
4.  x  :  \mBbbR{}
\mvdash{}  (\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}n  -  1\}  +  ((a  n)  *  x\^{}n))
=  (((\mSigma{}\{if  (i  =\msubz{}  0)  then  r0  else  rpolydiv(n;a;z)  (i  -  1)  fi    *  x\^{}i  |  0\mleq{}i\mleq{}n  -  1\}
    +  ((rpolydiv(n;a;z)  (n  -  1))  *  x\^{}n))
    +  \mSigma{}\{(-(z)  *  (rpolydiv(n;a;z)  i))  *  x\^{}i  |  0\mleq{}i\mleq{}n  -  1\})
    +  \mSigma{}\{(a  i)  *  z\^{}i  |  0\mleq{}i\mleq{}n\})


By

---

Latex:
((Subst'  rpolydiv(n;a;z)  (n  -  1)  \msim{}  a  n  0
    THENA  ((Unfold  `rpolydiv`  0  THEN  Reduce  0)
                  THEN  (Subst'  n  -  1  -  n  -  1  \msim{}  0  0  THENA  Auto)
                  THEN  Reduce  0
                  THEN  Auto)
    )
  THEN  (nRAdd  \mkleeneopen{}-((a  n)  *  x\^{}n)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  )

---

Home Index