---

Step * of Lemma add-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 THEN RepUR ``rpolynomial`` 0) }

1
1. n : ℕ
2. m : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. b : ℕm + 1 ⟶ ℝ
5. x : ℝ
6. m ≤ n
⊢ (Σ{(a i) * x^i | 0≤i≤n} + Σ{(b i) * x^i | 0≤i≤m}) = Σ{if i ≤z m then (a i) + (b i) else a i fi  * x^i | 0≤i≤n}

---

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  THEN  RepUR  ``rpolynomial``  0)

---

Home Index