---

Step * of Lemma rounded-numerator-property

∀[k:ℕ+]. ∀[r:ℚ].  |(k * r) - rounded-numerator(r;k)| < 1
BY
{ (Auto THEN (RW assert_pushupC 0 THENA Auto) THEN ((ElimOneRational⋅ THENA Auto) THEN ThinVar `r')⋅) }

1
1. k : ℕ+
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
⊢ ↑q_less(|(k * (p/q)) - rounded-numerator((p/q);k)|;1)

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbQ{}].    |(k  *  r)  -  rounded-numerator(r;k)|  <  1


By

---

Latex:
(Auto  THEN  (RW  assert\_pushupC  0  THENA  Auto)  THEN  ((ElimOneRational\mcdot{}  THENA  Auto)  THEN  ThinVar  `r')\mcdot{})

---

Home Index