---

Step * 2 1 1 of Lemma q-not-limit-zero-diverges-2


1. f : ℕ+ ⟶ ℚ
2. ∀n:ℕ+. (0 ≤ f[n])
3. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ f[m]))))
4. B : ℚ
5. n : ℕ
6. B ≤ Σ0 ≤ i < n. if (i =z 0) then 0 else f[i] fi 
7. n = 0 ∈ ℤ
⊢ Σ1 ≤ i < 0. f[i] = Σ0 ≤ i < 0. if (i =z 0) then 0 else f[i] fi  ∈ ℚ
BY
{ xxx((RW (AddrC [3] (LemmaC `sum_unroll_base_q`)) 0) THENA Auto)xxx }

1
1. f : ℕ+ ⟶ ℚ
2. ∀n:ℕ+. (0 ≤ f[n])
3. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ f[m]))))
4. B : ℚ
5. n : ℕ
6. B ≤ Σ0 ≤ i < n. if (i =z 0) then 0 else f[i] fi 
7. n = 0 ∈ ℤ
⊢ Σ1 ≤ i < 0. f[i] = 0 ∈ ℚ

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbQ{}
2.  \mforall{}n:\mBbbN{}\msupplus{}.  (0  \mleq{}  f[n])
3.  \mexists{}q:\mBbbQ{}.  (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  f[m]))))
4.  B  :  \mBbbQ{}
5.  n  :  \mBbbN{}
6.  B  \mleq{}  \mSigma{}0  \mleq{}  i  <  n.  if  (i  =\msubz{}  0)  then  0  else  f[i]  fi 
7.  n  =  0
\mvdash{}  \mSigma{}1  \mleq{}  i  <  0.  f[i]  =  \mSigma{}0  \mleq{}  i  <  0.  if  (i  =\msubz{}  0)  then  0  else  f[i]  fi 


By

---

Latex:
xxx((RW  (AddrC  [3]  (LemmaC  `sum\_unroll\_base\_q`))  0)  THENA  Auto)xxx

---

Home Index