---

Step * of Lemma rng_sum_shift

∀[r:Rng]. ∀[a,b:ℤ].
  ∀[E:{a..b-} ⟶ |r|]. ∀[k:ℤ].  ((Σ(r) a ≤ j < b. E[j]) = (Σ(r) a + k ≤ j < b + k. E[j - k]) ∈ |r|) supposing a ≤ b
BY
{ ProveSpecializedLemma `mon_itop_shift` 1 [parm{i};r↓+gp] (FoldC `rng_sum` ANDTHENC AbReduceC) }

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:\mBbbZ{}].
    \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  |r|].  \mforall{}[k:\mBbbZ{}].    ((\mSigma{}(r)  a  \mleq{}  j  <  b.  E[j])  =  (\mSigma{}(r)  a  +  k  \mleq{}  j  <  b  +  k.  E[j  -  k])) 
    supposing  a  \mleq{}  b


By

---

Latex:
ProveSpecializedLemma  `mon\_itop\_shift`  1  [parm\{i\};r\mdownarrow{}+gp]  (FoldC  `rng\_sum`  ANDTHENC  AbReduceC)

---

Home Index