---

Step * of Lemma shift-rpolynomial

No Annotations
∀[n:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[x:ℝ].
  ((x * (Σi≤n. a_i * x^i)) = (Σi≤n + 1. λi.if (i =z 0) then r0 else a (i - 1) fi _i * x^i))
BY
{ (Auto
   THEN (RWO "rmul-rpolynomial" 0 THENA Auto)
   THEN RepUR ``rpolynomial`` 0
   THEN (RW (AddrC [2] (LemmaC `rsum-split-first-shift`)) 0 THENA Auto)
   THEN Reduce 0) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    ((x  *  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))  =  (\mSigma{}i\mleq{}n  +  1.  \mlambda{}i.if  (i  =\msubz{}  0)  then  r0  else  a  (i  -  1)  fi  \_i  *  x\^{}i))


By

---

Latex:
(Auto
  THEN  (RWO  "rmul-rpolynomial"  0  THENA  Auto)
  THEN  RepUR  ``rpolynomial``  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `rsum-split-first-shift`))  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index