---

Step * 1 of Lemma qsum-delta

.....assertion..... 
∀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
BY
{ (((RepeatMFor 1 (D 0)) THENA Auto)
   THEN ((BLemma `int_le_to_int_upper` THENM BLemma `int_upper_ind`)
         THENA (Try (Complete (Auto))
                THEN RepeatFor 3 ((MemCD' THENA Auto))
                THEN Try (Complete (Auto))
                THEN SplitOnConclITE
                THEN Auto)
         )
   THEN Try ((Auto THEN (RWH (LemmaC `sum_unroll_base_q`) 0) THEN Try (Complete (Auto)) THEN SplitOnConclITE THEN Auto))
   THEN (D 0 THENA Auto)
   THEN (D 0 THENA (RepeatFor 2 ((MemCD' THENA Auto)) THEN Try (Complete (Auto)) THEN SplitOnConclITE THEN Auto))
   THEN RepeatFor 2 ((ParallelLast THEN (Thin (-3))))) }

1
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  ∈ ℚ

---

Latex:

---

Latex:
.....assertion..... 
\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


By

---

Latex:
(((RepeatMFor  1  (D  0))  THENA  Auto)
  THEN  ((BLemma  `int\_le\_to\_int\_upper`  THENM  BLemma  `int\_upper\_ind`)
              THENA  (Try  (Complete  (Auto))
                            THEN  RepeatFor  3  ((MemCD'  THENA  Auto))
                            THEN  Try  (Complete  (Auto))
                            THEN  SplitOnConclITE
                            THEN  Auto)
              )
  THEN  Try  ((Auto
                        THEN  (RWH  (LemmaC  `sum\_unroll\_base\_q`)  0)
                        THEN  Try  (Complete  (Auto))
                        THEN  SplitOnConclITE
                        THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (D  0
              THENA  (RepeatFor  2  ((MemCD'  THENA  Auto))
                            THEN  Try  (Complete  (Auto))
                            THEN  SplitOnConclITE
                            THEN  Auto)
              )
  THEN  RepeatFor  2  ((ParallelLast  THEN  (Thin  (-3)))))

---

Home Index