---

Step * of Lemma fractional-part_wf

∀q:ℚ. (fractional-part(q) ∈ {r:ℚ| (0 ≤ r) ∧ r < 1} )
BY
{ (ProveWfLemma THEN GenConclAtAddr [2;1] THEN D -2 THEN D -3 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (fractional-part(q)  \mmember{}  \{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  )


By

---

Latex:
(ProveWfLemma  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  D  -3  THEN  Reduce  0  THEN  Auto)

---

Home Index