---

Step * 2 1 of Lemma qsum-qle


1. ∀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
2. a : ℤ
3. b : ℤ
4. E : {a..b-} ⟶ ℚ
5. F : {a..b-} ⟶ ℚ
6. ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (E[j] ≤ F[j]))
7. ¬(a ≤ b)
⊢ Σa ≤ j < b. E[j] ≤ Σa ≤ j < b. F[j]
BY
{ (RepUR ``qsum rng_sum mon_itop`` 0 THEN RecUnfold `itop` 0 THEN (SplitOnConclITE THENA Auto) THEN Auto') }

---

Latex:

---

Latex:

1.  \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
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
5.  F  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
6.  \mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (E[j]  \mleq{}  F[j]))
7.  \mneg{}(a  \mleq{}  b)
\mvdash{}  \mSigma{}a  \mleq{}  j  <  b.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b.  F[j]


By

---

Latex:
(RepUR  ``qsum  rng\_sum  mon\_itop``  0
  THEN  RecUnfold  `itop`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Auto')

---

Home Index