---

Step * of Lemma qsum-non-neg2

∀[i,j:ℤ]. ∀[f:{i..j-} ⟶ ℚ].  0 ≤ Σi ≤ n < j. f[n] supposing ∀n:{i..j-}. (0 ≤ f[n])
BY
{ (Auto⋅
   THEN Assert ⌜Σi ≤ n < j. 0 ≤ Σi ≤ n < j. f[n]⌝⋅
   THEN Try ((BLemma `qsum-qle` THEN Auto))
   THEN Try (((RWO "qsum-const2" (-1)⋅ THEN Auto) THEN QNorm (-1)⋅ THEN Auto)⋅)) }

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[f:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].    0  \mleq{}  \mSigma{}i  \mleq{}  n  <  j.  f[n]  supposing  \mforall{}n:\{i..j\msupminus{}\}.  (0  \mleq{}  f[n])


By

---

Latex:
(Auto\mcdot{}
  THEN  Assert  \mkleeneopen{}\mSigma{}i  \mleq{}  n  <  j.  0  \mleq{}  \mSigma{}i  \mleq{}  n  <  j.  f[n]\mkleeneclose{}\mcdot{}
  THEN  Try  ((BLemma  `qsum-qle`  THEN  Auto))
  THEN  Try  (((RWO  "qsum-const2"  (-1)\mcdot{}  THEN  Auto)  THEN  QNorm  (-1)\mcdot{}  THEN  Auto)\mcdot{}))

---

Home Index