---

Step * 1 of Lemma qround-property


1. k : ℕ+
2. r : ℚ
⊢ |r - (rounded-numerator(r;2 * k)/2 * k)| < (1/|2 * k|)
BY
{ ((Assert 2 * k ∈ ℕ+ BY
          (RWW "qmul-mul" 0 THEN Auto))
   THEN (Assert 0 < |2 * k| BY
               ((RWO "qabs-abs" 0 THENA Auto) THEN (RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit))
   THEN ((QMul ⌜|2 * k|⌝ 0⋅ THENA Auto) THEN (RWO "qabs-qmul<" 0 THENA Auto)⋅ THEN QNorm 0)⋅) }

1
1. k : ℕ+
2. r : ℚ
3. 2 * k ∈ ℕ+
4. 0 < |2 * k|
⊢ |(2 * k * r) + -(rounded-numerator(r;2 * k))| < 1

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  r  :  \mBbbQ{}
\mvdash{}  |r  -  (rounded-numerator(r;2  *  k)/2  *  k)|  <  (1/|2  *  k|)


By

---

Latex:
((Assert  2  *  k  \mmember{}  \mBbbN{}\msupplus{}  BY
                (RWW  "qmul-mul"  0  THEN  Auto))
  THEN  (Assert  0  <  |2  *  k|  BY
                          ((RWO  "qabs-abs"  0  THENA  Auto)  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)  THEN  AutoSplit))
  THEN  ((QMul  \mkleeneopen{}|2  *  k|\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  (RWO  "qabs-qmul<"  0  THENA  Auto)\mcdot{}  THEN  QNorm  0)\mcdot{})

---

Home Index