---

Step * of Lemma qlog-bound

∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} .  ∃N:ℕ+. q ↑ N < e
BY
{ Auto }

1
1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
⊢ ∃N:ℕ+. q ↑ N < e

---

Latex:

---

Latex:
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}q:\{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\}  .    \mexists{}N:\mBbbN{}\msupplus{}.  q  \muparrow{}  N  <  e


By

---

Latex:
Auto

---

Home Index