---

Step * of Lemma item-rleq-rsum-of-nonneg

∀n,m:ℤ. ∀x:{n..m + 1-} ⟶ ℝ.  ((∀i:{n..m + 1-}. (r0 ≤ x[i])) ⇒ (∀i:{n..m + 1-}. (x[i] ≤ Σ{x[i] | n≤i≤m})))
BY
{ ((InstLemma `rsum-split` []⋅
    THEN RepeatFor 3 (ParallelLast')
    THEN (D 0 THENA Auto)
    THEN ParallelOp -2
    THEN (RWO "-1" 0 THENA Auto))
   THEN (Assert r0 ≤ Σ{x[i] | i + 1≤i≤m} BY
               ((BLemma `rsum_nonneg` THENM D 0) THEN Auto))
   THEN (RWO "-1<" 0 THENA Auto)
   THEN RWO "rsum-split-last" 0
   THEN Auto
   THEN (Assert r0 ≤ Σ{x[i] | n≤i≤i - 1} BY
               ((BLemma `rsum_nonneg` THENM D 0) THEN Auto))
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}i:\{n..m  +  1\msupminus{}\}.  (r0  \mleq{}  x[i]))  {}\mRightarrow{}  (\mforall{}i:\{n..m  +  1\msupminus{}\}.  (x[i]  \mleq{}  \mSigma{}\{x[i]  |  n\mleq{}i\mleq{}m\})))


By

---

Latex:
((InstLemma  `rsum-split`  []\mcdot{}
    THEN  RepeatFor  3  (ParallelLast')
    THEN  (D  0  THENA  Auto)
    THEN  ParallelOp  -2
    THEN  (RWO  "-1"  0  THENA  Auto))
  THEN  (Assert  r0  \mleq{}  \mSigma{}\{x[i]  |  i  +  1\mleq{}i\mleq{}m\}  BY
                          ((BLemma  `rsum\_nonneg`  THENM  D  0)  THEN  Auto))
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  RWO  "rsum-split-last"  0
  THEN  Auto
  THEN  (Assert  r0  \mleq{}  \mSigma{}\{x[i]  |  n\mleq{}i\mleq{}i  -  1\}  BY
                          ((BLemma  `rsum\_nonneg`  THENM  D  0)  THEN  Auto))
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index