---

Step * 2 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
⊢ ∀[a,b:ℤ]. ∀[E,F:{a..b-} ⟶ ℚ].
    Σa ≤ j < b. E[j] ≤ Σa ≤ j < b. F[j] supposing ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (E[j] ≤ F[j]))
BY
{ (Auto THEN Decide a ≤ b THEN Auto) }

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

---

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
\mvdash{}  \mforall{}[a,b:\mBbbZ{}].  \mforall{}[E,F:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].
        \mSigma{}a  \mleq{}  j  <  b.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b.  F[j]  supposing  \mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (E[j]  \mleq{}  F[j]))


By

---

Latex:
(Auto  THEN  Decide  a  \mleq{}  b  THEN  Auto)

---

Home Index