---

Step * 1 1 of Lemma rsum-as-itop


1. n : ℤ
2. m : ℤ
3. x : {n..m-} ⟶ ℝ
4. n < m
5. d : ℤ
6. n1 : ℤ
7. x1 : {n1..n1 + 0 + 1-} ⟶ ℝ
⊢ (Π(λx,y. (x + y),r0) n1 ≤ k < (n1 + 1) - 1. x1[k] + x1[(n1 + 1) - 1]) = Σ{x1[k] | n1≤k≤n1 + 0}
BY
{ ((RecUnfold `itop` 0 THEN (OReduce 0 THENA Auto))
   THEN ((Subst' n1 + 0 ~ n1 0 THENA Auto) THEN (Subst' (n1 + 1) - 1 ~ n1 0 THENA Auto))
   THEN RWO  "rsum-single" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  n  <  m
5.  d  :  \mBbbZ{}
6.  n1  :  \mBbbZ{}
7.  x1  :  \{n1..n1  +  0  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  (\mPi{}(\mlambda{}x,y.  (x  +  y),r0)  n1  \mleq{}  k  <  (n1  +  1)  -  1.  x1[k]  +  x1[(n1  +  1)  -  1])  =  \mSigma{}\{x1[k]  |  n1\mleq{}k\mleq{}n1  +  0\}


By

---

Latex:
((RecUnfold  `itop`  0  THEN  (OReduce  0  THENA  Auto))
  THEN  ((Subst'  n1  +  0  \msim{}  n1  0  THENA  Auto)  THEN  (Subst'  (n1  +  1)  -  1  \msim{}  n1  0  THENA  Auto))
  THEN  RWO    "rsum-single"  0
  THEN  Auto)

---

Home Index