---

Step * of Lemma rng_sum_0

∀[r:Rng]. ∀[a,b:ℤ].  (Σ(r) a ≤ j < b. 0) = 0 ∈ |r| supposing a ≤ b
BY
{ (InstLemma `rng_times_sum_l` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. r : Rng
2. a : ℤ
3. b : ℤ
4. a ≤ b
5. ∀[E:{a..b-} ⟶ |r|]. ∀[u:|r|].  ((u * (Σ(r) a ≤ j < b. E[j])) = (Σ(r) a ≤ j < b. u * E[j]) ∈ |r|)
⊢ (Σ(r) a ≤ j < b. 0) = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:\mBbbZ{}].    (\mSigma{}(r)  a  \mleq{}  j  <  b.  0)  =  0  supposing  a  \mleq{}  b


By

---

Latex:
(InstLemma  `rng\_times\_sum\_l`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index