---

Step * of Lemma subtract-rpolynomials

∀[n,m:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[b:ℕm + 1 ⟶ ℝ]. ∀[x:ℝ].
  ((Σi≤n. a_i * x^i) - (Σi≤m. b_i * x^i)) = (Σi≤n. λi.if i ≤z m then (a i) - b i else a i fi _i * x^i) supposing m ≤ n
BY
{ Auto }

1
1. n : ℕ
2. m : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. b : ℕm + 1 ⟶ ℝ
5. x : ℝ
6. m ≤ n
⊢ ((Σi≤n. a_i * x^i) - (Σi≤m. b_i * x^i)) = (Σi≤n. λi.if i ≤z m then (a i) - b i else a i fi _i * x^i)

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[b:\mBbbN{}m  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  -  (\mSigma{}i\mleq{}m.  b\_i  *  x\^{}i))
    =  (\mSigma{}i\mleq{}n.  \mlambda{}i.if  i  \mleq{}z  m  then  (a  i)  -  b  i  else  a  i  fi  \_i  *  x\^{}i) 
    supposing  m  \mleq{}  n


By

---

Latex:
Auto

---

Home Index