---

Step * of Lemma qsum-non-neg

∀[j:ℕ]. ∀[f:ℕj ⟶ ℚ].  0 ≤ Σ0 ≤ n < j. f[n] supposing ∀n:ℕj. (0 ≤ f[n])
BY
{ (Auto⋅ THEN Assert ⌜Σ0 ≤ n < j. 0 ≤ Σ0 ≤ n < j. f[n]⌝⋅) }

1
.....assertion..... 
1. j : ℕ
2. f : ℕj ⟶ ℚ
3. ∀n:ℕj. (0 ≤ f[n])
⊢ Σ0 ≤ n < j. 0 ≤ Σ0 ≤ n < j. f[n]

2
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]

---

Latex:

---

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


By

---

Latex:
(Auto\mcdot{}  THEN  Assert  \mkleeneopen{}\mSigma{}0  \mleq{}  n  <  j.  0  \mleq{}  \mSigma{}0  \mleq{}  n  <  j.  f[n]\mkleeneclose{}\mcdot{})

---

Home Index