---

Step * of Lemma sum_unroll_base_q

No Annotations
∀[i,j:ℤ].  ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = 0 ∈ ℚ) supposing i = j ∈ ℤ
BY
{ ((ProveSpecializedLemmaWReduce rng_sum_unroll_base) 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]  =  0)  supposing  i  =  j


By

---

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

---

Home Index