---

Step * 1 of Lemma qsum-qle

.....assertion..... 
∀a,b:ℤ.
  ∀E,F:{a..b-} ⟶ ℚ.  ((∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (E[j] ≤ F[j]))) ⇒ (Σa ≤ j < b. E[j] ≤ Σa ≤ j < b. F[j])) 
  supposing a ≤ b
BY
{ (((RepeatMFor 1 (D 0)) THENA Auto)
   THEN (BLemma `int_le_to_int_upper` THENA Auto)
   THEN (((BLemma `int_upper_ind` THENA Auto) THEN UnivCD) THENA Auto)) }

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

2
1. a : ℤ
2. b : {a + 1...}
3. ∀E,F:{a..b - 1-} ⟶ ℚ.
     ((∀j@0:ℤ. ((a ≤ j@0) ⇒ j@0 < b - 1 ⇒ (E[j@0] ≤ F[j@0]))) ⇒ (Σa ≤ j < b - 1. E[j] ≤ Σa ≤ j < b - 1. F[j]))
4. E : {a..b-} ⟶ ℚ
5. F : {a..b-} ⟶ ℚ
6. ∀j@0:ℤ. ((a ≤ j@0) ⇒ j@0 < b ⇒ (E[j@0] ≤ F[j@0]))
⊢ Σa ≤ j < b. E[j] ≤ Σa ≤ j < b. F[j]

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}a,b:\mBbbZ{}.
    \mforall{}E,F:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}.
        ((\mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (E[j]  \mleq{}  F[j])))  {}\mRightarrow{}  (\mSigma{}a  \mleq{}  j  <  b.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b.  F[j])) 
    supposing  a  \mleq{}  b


By

---

Latex:
(((RepeatMFor  1  (D  0))  THENA  Auto)
  THEN  (BLemma  `int\_le\_to\_int\_upper`  THENA  Auto)
  THEN  (((BLemma  `int\_upper\_ind`  THENA  Auto)  THEN  UnivCD)  THENA  Auto))

---

Home Index