---

Step * 1 of Lemma summand-qle-sum


1. a : ℤ
2. b : ℤ
3. E : {a..b-} ⟶ ℚ
4. ∀j:{a..b-}. (0 ≤ E[j])
5. i : {a..b-}
6. Σa ≤ j < b. E[j] * delta(i;j) = E[i] ∈ ℚ
7. a ≤ i
8. i < b
9. j : ℤ
10. a ≤ j
11. j < b
⊢ (E[j] * delta(i;j)) ≤ E[j]
BY
{ (Unfold `delta` 0 THEN (SplitOnConclITE THEN Auto) THEN QNorm 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
4.  \mforall{}j:\{a..b\msupminus{}\}.  (0  \mleq{}  E[j])
5.  i  :  \{a..b\msupminus{}\}
6.  \mSigma{}a  \mleq{}  j  <  b.  E[j]  *  delta(i;j)  =  E[i]
7.  a  \mleq{}  i
8.  i  <  b
9.  j  :  \mBbbZ{}
10.  a  \mleq{}  j
11.  j  <  b
\mvdash{}  (E[j]  *  delta(i;j))  \mleq{}  E[j]


By

---

Latex:
(Unfold  `delta`  0  THEN  (SplitOnConclITE  THEN  Auto)  THEN  QNorm  0  THEN  Auto)\mcdot{}

---

Home Index