---

Step * 1 of Lemma add-rpolynomials


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}
BY
{ ((InstLemma `rsum-split-shift` [⌜m⌝;⌜0⌝;⌜n⌝;⌜λ2i.(a i) * x^i⌝]⋅ THENA Auto) THEN (RWO  "-1" 0 THENA Auto)) }

1
1. n : ℕ
2. m : ℕ
3. a : ℕn + 1 ⟶ ℝ
4. b : ℕm + 1 ⟶ ℝ
5. x : ℝ
6. m ≤ n
7. Σ{(a i) * x^i | 0≤i≤n} = (Σ{(a i) * x^i | 0≤i≤m} + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1})
⊢ ((Σ{(a i) * x^i | 0≤i≤m} + Σ{(a (m + i + 1)) * x^m + i + 1 | 0≤i≤n - m + 1}) + Σ{(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:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  a  :  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}
4.  b  :  \mBbbN{}m  +  1  {}\mrightarrow{}  \mBbbR{}
5.  x  :  \mBbbR{}
6.  m  \mleq{}  n
\mvdash{}  (\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}n\}  +  \mSigma{}\{(b  i)  *  x\^{}i  |  0\mleq{}i\mleq{}m\})
=  \mSigma{}\{if  i  \mleq{}z  m  then  (a  i)  +  (b  i)  else  a  i  fi    *  x\^{}i  |  0\mleq{}i\mleq{}n\}


By

---

Latex:
((InstLemma  `rsum-split-shift`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.(a  i)  *  x\^{}i\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO    "-1"  0  THENA  Auto)
  )

---

Home Index