---

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

∀f:ℕ+ ⟶ ℚ
  (∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ f[m]))))) ⇒ (∀B:ℚ. ∃n:ℕ. (B ≤ Σ1 ≤ i < n. f[i])) 
  supposing ∀n:ℕ+. (0 ≤ f[n])
BY
{ xxx(Auto THEN (InstLemma `q-not-limit-zero-diverges` [⌜λ2n.if (n =z 0) then 0 else f[n] fi ⌝;⌜B⌝]⋅ THENA Auto))xxx }

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

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

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbQ{}
    (\mexists{}q:\mBbbQ{}.  (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  f[m])))))  {}\mRightarrow{}  (\mforall{}B:\mBbbQ{}.  \mexists{}n:\mBbbN{}.  (B  \mleq{}  \mSigma{}1  \mleq{}  i  <  n.  f[i])) 
    supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (0  \mleq{}  f[n])


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `q-not-limit-zero-diverges`
                    [\mkleeneopen{}\mlambda{}\msubtwo{}n.if  (n  =\msubz{}  0)  then  0  else  f[n]  fi  \mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
                    THENA  Auto
                    )
        )xxx

---

Home Index