---

Step * of Lemma rng_sum_split

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

---

Latex:

---

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


By

---

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

---

Home Index