---

Step * 1 2 1 1 of Lemma qsum-qle


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]))
7. E[b - 1] ≤ F[b - 1]
8. Σa ≤ j < b - 1. E[j] ≤ Σa ≤ j < b - 1. F[j]
⊢ (Σa ≤ j < b - 1. E[j] + E[b - 1]) ≤ (Σa ≤ j < b - 1. F[j] + F[b - 1])
BY
{ xxx(((Assert (Σa ≤ j < b - 1. E[j] + E[b - 1]) ≤ (Σa ≤ j < b - 1. E[j] + F[b - 1]) BY
              (BLemma `grp_op_preserves_le_qorder` THEN Auto))
       THEN (Assert (Σa ≤ j < b - 1. E[j] + F[b - 1]) ≤ (Σa ≤ j < b - 1. F[j] + F[b - 1]) BY
                   (RWO "qadd_com" 0 THENM (BLemma `grp_op_preserves_le_qorder` THEN Auto)))
       )
      THEN Auto
      )xxx }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \{a  +  1...\}
3.  \mforall{}E,F:\{a..b  -  1\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}.
          ((\mforall{}j@0:\mBbbZ{}.  ((a  \mleq{}  j@0)  {}\mRightarrow{}  j@0  <  b  -  1  {}\mRightarrow{}  (E[j@0]  \mleq{}  F[j@0])))
          {}\mRightarrow{}  (\mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b  -  1.  F[j]))
4.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
5.  F  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
6.  \mforall{}j@0:\mBbbZ{}.  ((a  \mleq{}  j@0)  {}\mRightarrow{}  j@0  <  b  {}\mRightarrow{}  (E[j@0]  \mleq{}  F[j@0]))
7.  E[b  -  1]  \mleq{}  F[b  -  1]
8.  \mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  \mleq{}  \mSigma{}a  \mleq{}  j  <  b  -  1.  F[j]
\mvdash{}  (\mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  +  E[b  -  1])  \mleq{}  (\mSigma{}a  \mleq{}  j  <  b  -  1.  F[j]  +  F[b  -  1])


By

---

Latex:
xxx(((Assert  (\mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  +  E[b  -  1])  \mleq{}  (\mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  +  F[b  -  1])  BY
                        (BLemma  `grp\_op\_preserves\_le\_qorder`  THEN  Auto))
          THEN  (Assert  (\mSigma{}a  \mleq{}  j  <  b  -  1.  E[j]  +  F[b  -  1])  \mleq{}  (\mSigma{}a  \mleq{}  j  <  b  -  1.  F[j]  +  F[b  -  1])  BY
                                  (RWO  "qadd\_com"  0  THENM  (BLemma  `grp\_op\_preserves\_le\_qorder`  THEN  Auto)))
          )
        THEN  Auto
        )xxx

---

Home Index