---

Step * of Lemma sum_unroll_hi_q

No Annotations
∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = (Σi ≤ k < j - 1. E[k] + E[j - 1]) ∈ ℚ) supposing i < j
BY
{ ((ProveSpecializedLemmaWReduce rng_sum_unroll_hi) 0 [⌜parm{i}⌝;⌜<ℚ+*>⌝]⋅ THEN Fold `qsum` (-1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[i,j:\mBbbZ{}].    \mforall{}[E:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].  (\mSigma{}i  \mleq{}  k  <  j.  E[k]  =  (\mSigma{}i  \mleq{}  k  <  j  -  1.  E[k]  +  E[j  -  1]))  supposing  i  <  j


By

---

Latex:
((ProveSpecializedLemmaWReduce  rng\_sum\_unroll\_hi)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+*>\mkleeneclose{}]\mcdot{}
  THEN  Fold  `qsum`  (-1)
  THEN  Auto)

---

Home Index