---

Step * of Lemma qsum-delta

∀[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  ∈ ℚ)
BY
{ Assert ⌜∀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⌝⋅ }

1
.....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

2
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
⊢ ∀[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  ∈ ℚ)

---

Latex:

---

Latex:
\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  )


By

---

Latex:
Assert  \mkleeneopen{}\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\mkleeneclose{}\mcdot{}

---

Home Index