---

Step * 1 of Lemma shift-rpolynomial


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})
BY
{ ((nRNorm 0 THENA Auto) THEN (Subst' (n + 1) - 1 ~ n 0 THEN Auto) THEN (BLemma `rsum_functionality`  THENA Auto)) }

1
1. n : ℕ
2. a : ℕn + 1 ⟶ ℝ
3. x : ℝ
⊢ (a i) * x^i * x = if (i + 1 =z 0) then r0 else a ((i + 1) - 1) fi  * x^i + 1 for i ∈ [0,n]

---

Latex:

---

Latex:

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


By

---

Latex:
((nRNorm  0  THENA  Auto)
  THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  0  THEN  Auto)
  THEN  (BLemma  `rsum\_functionality`    THENA  Auto))

---

Home Index