---

Step * of Lemma reciprocal-qle-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)  \mleq{}  e)  supposing  0  <  e


By

---

Latex:
xxx(Auto  THEN  ElimRationals  THEN  Auto)xxx

---

Home Index