---

Step * of Lemma integer-fractional-parts

∀q:ℚ. (q = (integer-part(q) + fractional-part(q)) ∈ ℚ)
BY
{ xxx(Auto
      THEN RepUR ``integer-part fractional-part`` 0
      THEN GenConclAtAddr [3;1;1]
      THEN D -2
      THEN D -3
      THEN All Reduce
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (q  =  (integer-part(q)  +  fractional-part(q)))


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``integer-part  fractional-part``  0
        THEN  GenConclAtAddr  [3;1;1]
        THEN  D  -2
        THEN  D  -3
        THEN  All  Reduce
        THEN  Auto)xxx

---

Home Index