---

Step * 1 1 of Lemma qsum-qle


1. a : ℤ
2. E : {a..a-} ⟶ ℚ
3. F : {a..a-} ⟶ ℚ
4. ∀j@0:ℤ. ((a ≤ j@0) ⇒ j@0 < a ⇒ (E[j@0] ≤ F[j@0]))
⊢ Σa ≤ j < a. E[j] ≤ Σa ≤ j < a. F[j]
BY
{ ((RWH (LemmaC `sum_unroll_base_q`) 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  E  :  \{a..a\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
3.  F  :  \{a..a\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
4.  \mforall{}j@0:\mBbbZ{}.  ((a  \mleq{}  j@0)  {}\mRightarrow{}  j@0  <  a  {}\mRightarrow{}  (E[j@0]  \mleq{}  F[j@0]))
\mvdash{}  \mSigma{}a  \mleq{}  j  <  a.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  a.  F[j]


By

---

Latex:
((RWH  (LemmaC  `sum\_unroll\_base\_q`)  0)  THEN  Auto)\mcdot{}

---

Home Index