---

Step * of Lemma qsum-qle

∀[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
{ Assert ⌜∀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⌝⋅ }

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

2
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]))

---

Latex:

---

Latex:
\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:
Assert  \mkleeneopen{}\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\mkleeneclose{}\mcdot{}

---

Home Index