---

Step * of Lemma small-reciprocal-proof

∀e:ℚ. ∃m:ℕ+. (1/m) < e supposing 0 < e
BY
{ xxx(Auto THEN ElimRationals THEN Auto)xxx }

1
1. e : ℚ
2. 0 < e
3. p : ℤ
4. q : ℤ
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. e = (p/q) ∈ ℚ
8. ¬↑qeq(q;0)
⊢ ∃m:ℕ+. (1/m) < (p/q)

---

Latex:

---

Latex:
\mforall{}e:\mBbbQ{}.  \mexists{}m:\mBbbN{}\msupplus{}.  (1/m)  <  e  supposing  0  <  e


By

---

Latex:
xxx(Auto  THEN  ElimRationals  THEN  Auto)xxx

---

Home Index