---

Step * 1 1 of Lemma add-rpolynomials


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}
BY
{ ((InstLemma `rsum-split-shift` [⌜m⌝;⌜0⌝;⌜n⌝;⌜λ2i.if i ≤z m then (a i) + (b i) else a i fi  * 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})
8. Σ{if i ≤z m then (a i) + (b i) else a i fi  * x^i | 0≤i≤n}
= (Σ{if i ≤z m then (a i) + (b i) else a i fi  * x^i | 0≤i≤m}
  + Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi  * 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≤m}
  + Σ{if m + i + 1 ≤z m then (a (m + i + 1)) + (b (m + i + 1)) else a (m + i + 1) fi  * x^m + i + 1 | 0≤i≤n - m + 1})

---

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
7.  \mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}n\}
=  (\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}m\}  +  \mSigma{}\{(a  (m  +  i  +  1))  *  x\^{}m  +  i  +  1  |  0\mleq{}i\mleq{}n  -  m  +  1\})
\mvdash{}  ((\mSigma{}\{(a  i)  *  x\^{}i  |  0\mleq{}i\mleq{}m\}  +  \mSigma{}\{(a  (m  +  i  +  1))  *  x\^{}m  +  i  +  1  |  0\mleq{}i\mleq{}n  -  m  +  1\})
+  \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.if  i  \mleq{}z  m  then  (a  i)  +  (b  i)  else  a  i  fi    *  x\^{}i\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (RWO    "-1"  0  THENA  Auto)
  )

---

Home Index