---

Step * of Lemma qround-property

No Annotations
∀[k:ℕ+]. ∀[r:ℚ].  |r - qround(r;k)| < (1/2 * k)
BY
{ (Auto
   THEN (RWO "qround-eq" 0 THENA Auto)
   THEN (Subst ⌜(1/2 * k) = (1/|2 * k|) ∈ ℚ⌝ 0⋅
         THENA (Auto
                THEN (RWO "qabs-of-positive" 0 THEN Auto)
                THEN (RWO "qmul-mul<" 0 THENA Auto)
                THEN QMul ⌜k⌝ 0⋅
                THEN Auto)
         )⋅) }

1
1. k : ℕ+
2. r : ℚ
⊢ |r - (rounded-numerator(r;2 * k)/2 * k)| < (1/|2 * k|)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbQ{}].    |r  -  qround(r;k)|  <  (1/2  *  k)


By

---

Latex:
(Auto
  THEN  (RWO  "qround-eq"  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(1/2  *  k)  =  (1/|2  *  k|)\mkleeneclose{}  0\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "qabs-of-positive"  0  THEN  Auto)
                            THEN  (RWO  "qmul-mul<"  0  THENA  Auto)
                            THEN  QMul  \mkleeneopen{}k\mkleeneclose{}  0\mcdot{}
                            THEN  Auto)
              )\mcdot{})

---

Home Index