---

Step * 2 of Lemma qsum-non-neg


1. j : ℕ
2. f : ℕj ⟶ ℚ
3. ∀n:ℕj. (0 ≤ f[n])
4. Σ0 ≤ n < j. 0 ≤ Σ0 ≤ n < j. f[n]
⊢ 0 ≤ Σ0 ≤ n < j. f[n]
BY
{ ((RWO "qsum-const" (-1)⋅ THEN Auto) THEN QNorm (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  j  :  \mBbbN{}
2.  f  :  \mBbbN{}j  {}\mrightarrow{}  \mBbbQ{}
3.  \mforall{}n:\mBbbN{}j.  (0  \mleq{}  f[n])
4.  \mSigma{}0  \mleq{}  n  <  j.  0  \mleq{}  \mSigma{}0  \mleq{}  n  <  j.  f[n]
\mvdash{}  0  \mleq{}  \mSigma{}0  \mleq{}  n  <  j.  f[n]


By

---

Latex:
((RWO  "qsum-const"  (-1)\mcdot{}  THEN  Auto)  THEN  QNorm  (-1)\mcdot{}  THEN  Auto)

---

Home Index