---

Step * of Lemma sum_unroll_unit_q

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


By

---

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

---

Home Index