---

Step * of Lemma rsum_nonneg

∀[n,m:ℤ]. ∀[y:{n..m + 1-} ⟶ ℝ].  r0 ≤ Σ{y[k] | n≤k≤m} supposing r0 ≤ y[k] for k ∈ [n,m]
BY
{ (Auto THEN (Assert r0 = Σ{r0 | n≤k≤m} BY (Auto THEN RWO "rsum-zero" 0 THEN Auto)) THEN RWO "-1" 0 THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].  \mforall{}[y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].    r0  \mleq{}  \mSigma{}\{y[k]  |  n\mleq{}k\mleq{}m\}  supposing  r0  \mleq{}  y[k]  for  k  \mmember{}  [n,m]


By

---

Latex:
(Auto
  THEN  (Assert  r0  =  \mSigma{}\{r0  |  n\mleq{}k\mleq{}m\}  BY
                          (Auto  THEN  RWO  "rsum-zero"  0  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  EAuto  1)

---

Home Index