---

Step * 1 of Lemma rounded-numerator-property


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)
BY
{ (RepUR ``q_less rounded-numerator qdiv qabs qinv qmul qsub qadd qeq qpositive`` 0⋅
   THEN (CallByValueReduceOn ⌜k⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜p⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜q⌝ 0⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN (CallByValueReduceOn ⌜<1, q>⌝ 0⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN (CallByValueReduceOn ⌜<p * 1, q>⌝ 0⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)
   THEN (CallByValueReduceOn ⌜<k * p * 1, q>⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜((p * 1) * k) ÷ q⌝ 0⋅ THENA Auto)
   THEN (Subst' isint(((p * 1) * k) ÷ q) ~ tt 0 THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜(-1) * (((p * 1) * k) ÷ q)⌝ 0⋅ THENA Auto)
   THEN (Subst' isint((-1) * (((p * 1) * k) ÷ q)) ~ tt 0 THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜<(k * p * 1) + (((-1) * (((p * 1) * k) ÷ q)) * q), q>⌝ 0⋅ THENA Auto)
   THEN (OReduce 0 THENW Auto)
   THEN Repeat (AutoSplit)
   THEN (RW assert_pushdownC 0 THEN Auto)⋅
   THEN All (RW IntNormC)
   THEN Auto) }

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

2
1. k : ℕ+
2. p : ℤ
3. q : ℤ
4. ¬0 < (k * p) + ((-1) * q * ((k * p) ÷ q))
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. (k * p) + ((-1) * q * ((k * p) ÷ q)) < 0
⊢ ((-1) * k * p) + (q * ((k * p) ÷ q)) < q

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  p  :  \mBbbZ{}
3.  q  :  \mBbbZ{}
4.  0  <  q
5.  \mneg{}(q  =  0)
6.  \mneg{}\muparrow{}qeq(q;0)
\mvdash{}  \muparrow{}q\_less(|(k  *  (p/q))  -  rounded-numerator((p/q);k)|;1)


By

---

Latex:
(RepUR  ``q\_less  rounded-numerator  qdiv  qabs  qinv  qmul  qsub  qadd  qeq  qpositive``  0\mcdot{}
  THEN  (CallByValueReduceOn  \mkleeneopen{}k\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}p\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}q\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}ə,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}<p  *  1,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}<k  *  p  *  1,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}((p  *  1)  *  k)  \mdiv{}  q\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  isint(((p  *  1)  *  k)  \mdiv{}  q)  \msim{}  tt  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}(-1)  *  (((p  *  1)  *  k)  \mdiv{}  q)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst'  isint((-1)  *  (((p  *  1)  *  k)  \mdiv{}  q))  \msim{}  tt  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}<(k  *  p  *  1)  +  (((-1)  *  (((p  *  1)  *  k)  \mdiv{}  q))  *  q),  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (OReduce  0  THENW  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  (RW  assert\_pushdownC  0  THEN  Auto)\mcdot{}
  THEN  All  (RW  IntNormC)
  THEN  Auto)

---

Home Index