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