---

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

∀f:ℕ ⟶ ℚ
  (∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (q ≤ f[m]))))) ⇒ (∀B:ℚ. ∃n:ℕ. (B ≤ Σ0 ≤ i < n. f[i])) 
  supposing ∀n:ℕ. (0 ≤ f[n])
BY
{ ((Auto THEN ExRepD) THEN RenameVar `c' 5) }

1
1. f : ℕ ⟶ ℚ
2. ∀n:ℕ. (0 ≤ f[n])
3. q : ℚ
4. 0 < q
5. c : ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (q ≤ f[m]))
6. B : ℚ
⊢ ∃n:ℕ. (B ≤ Σ0 ≤ i < n. f[i])

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  ExRepD)  THEN  RenameVar  `c'  5)

---

Home Index