---

Step * of Lemma reduce-real_wf

∀[k:ℕ+]. ∀[x:ℝ]. ∀[b:{b:ℝ| r0 < b} ].  (reduce-real(x;b;k) ∈ {n:ℤ| |x - r(n) * b| ≤ (b + (b/r(k)))} )
BY
{ (Auto
   THEN (Assert r0 < b BY
               (D -1 THEN Unhide THEN Auto))
   THEN Unfold `reduce-real` 0
   THEN DoSubsume
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (Assert |b| = b BY
               (RWO  "rabs-of-nonneg" 0 THEN Auto))
   THEN nRMul ⌜|b|⌝ (-2)⋅
   THEN Auto
   THEN (RWO  "rabs-rmul<" (-2) THENA Auto)
   THEN nRNorm (-2)
   THEN nRNorm 0
   THEN (RWO "-2" 0 THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  r0  <  b\}  ].    (reduce-real(x;b;k)  \mmember{}  \{n:\mBbbZ{}|  |x  -  r(n)  *  b|  \mleq{}  (b  +  (b/r(k)))\}  \000C)


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  b  BY
                          (D  -1  THEN  Unhide  THEN  Auto))
  THEN  Unfold  `reduce-real`  0
  THEN  DoSubsume
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Assert  |b|  =  b  BY
                          (RWO    "rabs-of-nonneg"  0  THEN  Auto))
  THEN  nRMul  \mkleeneopen{}|b|\mkleeneclose{}  (-2)\mcdot{}
  THEN  Auto
  THEN  (RWO    "rabs-rmul<"  (-2)  THENA  Auto)
  THEN  nRNorm  (-2)
  THEN  nRNorm  0
  THEN  (RWO  "-2"  0  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index