---

Step * 1 of Lemma rpolynomial-rmul


1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [x] : ℝ
4. [b] : ℝ
5. (b * (Σi≤n. a_i * x^i)) = (Σi≤n. λi.(b * (a i))_i * x^i)
⊢ ((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i)
BY
{ (Assert (b * (Σi≤n. a_i * x^i)) = ((Σi≤n. a_i * x^i) * b) BY
         Auto) }

1
1. [n] : ℕ
2. [a] : ℕn + 1 ⟶ ℝ
3. [x] : ℝ
4. [b] : ℝ
5. (b * (Σi≤n. a_i * x^i)) = (Σi≤n. λi.(b * (a i))_i * x^i)
6. (b * (Σi≤n. a_i * x^i)) = ((Σi≤n. a_i * x^i) * b)
⊢ ((Σi≤n. a_i * x^i) * b) = (Σi≤n. λi.((a i) * b)_i * x^i)

---

Latex:

---

Latex:

1.  [n]  :  \mBbbN{}
2.  [a]  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
3.  [x]  :  \mBbbR{}
4.  [b]  :  \mBbbR{}
5.  (b  *  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.(b  *  (a  i))\_i  *  x\^{}i)
\mvdash{}  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  *  b)  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  *  b)\_i  *  x\^{}i)


By

---

Latex:
(Assert  (b  *  (\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i))  =  ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  *  b)  BY
              Auto)

---

Home Index