---

Step * 1 of Lemma rsum-as-itop


1. n : ℤ
2. m : ℤ
3. x : {n..m-} ⟶ ℝ
4. n < m
⊢ Π(λx,y. (x + y),r0) n ≤ k < m. x[k] = Σ{x[k] | n≤k≤m - 1}
BY
{ ((Assert ⌜∀d:ℕ. ∀n:ℤ. ∀x:{n..n + d + 1-} ⟶ ℝ.  (Π(λx,y. (x + y),r0) n ≤ k < n + d + 1. x[k] = Σ{x[k] | n≤k≤n + d})⌝⋅
   THENM ((InstHyp [⌜m - n - 1⌝;⌜n⌝;⌜x⌝] (-1)⋅ THENM NthHypSq (-1)) THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto
   THEN RecUnfold `itop` 0
   THEN (OReduce 0 THENA Auto)) }

1
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}

2
1. n : ℤ
2. m : ℤ
3. x : {n..m-} ⟶ ℝ
4. n < m
5. d : ℤ
6. 0 < d
7. ∀n:ℤ. ∀x:{n..n + (d - 1) + 1-} ⟶ ℝ.  (Π(λx,y. (x + y),r0) n ≤ k < n + (d - 1) + 1. x[k] = Σ{x[k] | n≤k≤n + (d - 1)})
8. n1 : ℤ
9. x1 : {n1..n1 + d + 1-} ⟶ ℝ
⊢ (Π(λx,y. (x + y),r0) n1 ≤ k < (n1 + d + 1) - 1. x1[k] + x1[(n1 + d + 1) - 1]) = Σ{x1[k] | n1≤k≤n1 + d}

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}n:\mBbbZ{}.  \mforall{}x:\{n..n  +  d  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
                        (\mPi{}(\mlambda{}x,y.  (x  +  y),r0)  n  \mleq{}  k  <  n  +  d  +  1.  x[k]  =  \mSigma{}\{x[k]  |  n\mleq{}k\mleq{}n  +  d\})\mkleeneclose{}\mcdot{}
  THENM  ((InstHyp  [\mkleeneopen{}m  -  n  -  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENM  NthHypSq  (-1))  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto
  THEN  RecUnfold  `itop`  0
  THEN  (OReduce  0  THENA  Auto))

---

Home Index