---

Step * 2 1 of Lemma qsum-delta


1. ∀a,b:ℤ.
     ∀E:{a..b-} ⟶ ℚ. ∀i:ℤ.  (Σa ≤ j < b. E[j] * delta(i;j) = if a ≤z i ∧b i <z b then E[i] else 0 fi  ∈ ℚ) 
     supposing a ≤ b
2. a : ℤ
3. b : ℤ
4. E : {a..b-} ⟶ ℚ
5. i : ℤ
6. ¬(a ≤ b)
⊢ Σa ≤ j < b. E[j] * delta(i;j) = if a ≤z i ∧b i <z b then E[i] else 0 fi  ∈ ℚ
BY
{ TACTIC:(RepUR ``qsum rng_sum mon_itop`` 0 THEN RecUnfold `itop` 0 THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:

1.  \mforall{}a,b:\mBbbZ{}.
          \mforall{}E:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}.  \mforall{}i:\mBbbZ{}.
              (\mSigma{}a  \mleq{}  j  <  b.  E[j]  *  delta(i;j)  =  if  a  \mleq{}z  i  \mwedge{}\msubb{}  i  <z  b  then  E[i]  else  0  fi  ) 
          supposing  a  \mleq{}  b
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
5.  i  :  \mBbbZ{}
6.  \mneg{}(a  \mleq{}  b)
\mvdash{}  \mSigma{}a  \mleq{}  j  <  b.  E[j]  *  delta(i;j)  =  if  a  \mleq{}z  i  \mwedge{}\msubb{}  i  <z  b  then  E[i]  else  0  fi 


By

---

Latex:
TACTIC:(RepUR  ``qsum  rng\_sum  mon\_itop``  0  THEN  RecUnfold  `itop`  0  THEN  Repeat  (AutoSplit))

---

Home Index