---

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

.....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 ))))
BY
{ xxx(ExRepD THEN (InstConcl [⌜q⌝]⋅ THENA Auto) THEN D 0 THEN Try (Trivial))xxx }

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

---

Latex:

---

Latex:
.....antecedent..... 
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{}
\mvdash{}  \mexists{}q:\mBbbQ{}.  (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  (q  \mleq{}  if  (m  =\msubz{}  0)  then  0  else  f[m]  fi  ))))


By

---

Latex:
xxx(ExRepD  THEN  (InstConcl  [\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  0  THEN  Try  (Trivial))xxx

---

Home Index