---

Step * 1 1 of Lemma qsum-delta


1. a : ℤ
2. b : {a + 1...}
3. E : {a..b-} ⟶ ℚ
4. i : ℤ
5. Σa ≤ j < b - 1. E[j] * delta(i;j) = if a ≤z i ∧b i <z b - 1 then E[i] else 0 fi  ∈ ℚ
⊢ Σa ≤ j < b. E[j] * delta(i;j) = if a ≤z i ∧b i <z b then E[i] else 0 fi  ∈ ℚ
BY
{ ((SplitOnHypITE -1  THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN SplitOrHyps
   THEN Auto'
   THEN (RWH (LemmaC `sum_unroll_hi_q`) 0)
   THEN Auto
   THEN OnMaybeHyp 5 (\h.
   ((HypSubst h 0 THENA Auto) THEN Unfold `delta` 0 THEN SplitOnConclITE THEN Auto' THEN QNorm 0))
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \{a  +  1...\}
3.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
4.  i  :  \mBbbZ{}
5.  \mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  *  delta(i;j)  =  if  a  \mleq{}z  i  \mwedge{}\msubb{}  i  <z  b  -  1  then  E[i]  else  0  fi 
\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:
((SplitOnHypITE  -1    THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Auto'
  THEN  (RWH  (LemmaC  `sum\_unroll\_hi\_q`)  0)
  THEN  Auto
  THEN  OnMaybeHyp  5  (\mbackslash{}h.  ((HypSubst  h  0  THENA  Auto)
                                                  THEN  Unfold  `delta`  0
                                                  THEN  SplitOnConclITE
                                                  THEN  Auto'
                                                  THEN  QNorm  0))
  THEN  Auto)

---

Home Index