---

Step * of Lemma fractional-part-rep

∀r:{r:ℚ| (0 ≤ r) ∧ r < 1} . ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ (r = (a/b) ∈ ℚ))
BY
{ (Auto THEN D -1 THEN (Assert (0 ≤ r) ∧ r < 1 BY (Unhide THEN Auto)) THEN Thin (-2))⋅ }

1
1. r : ℚ
2. (0 ≤ r) ∧ r < 1
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ (r = (a/b) ∈ ℚ))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  -1  THEN  (Assert  (0  \mleq{}  r)  \mwedge{}  r  <  1  BY  (Unhide  THEN  Auto))  THEN  Thin  (-2))\mcdot{}

---

Home Index