---

Step * 1 of Lemma fractional-part-rep


1. r : ℚ
2. (0 ≤ r) ∧ r < 1
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ (r = (a/b) ∈ ℚ))
BY
{ (ElimRationals THEN Auto) }

1
1. r : ℚ
2. 0 ≤ r
3. r < 1
4. p : ℤ
5. q : ℤ
6. 0 < q
7. ¬(q = 0 ∈ ℚ)
8. r = (p/q) ∈ ℚ
9. ¬↑qeq(q;0)
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  (0  \mleq{}  r)  \mwedge{}  r  <  1
\mvdash{}  \mexists{}a,b:\mBbbN{}.  ((0  \mleq{}  a)  \mwedge{}  a  <  b  \mwedge{}  (r  =  (a/b)))


By

---

Latex:
(ElimRationals  THEN  Auto)

---

Home Index