---

Step * of Lemma proportional-round-property

∀[k,l:ℕ+]. ∀[r:ℚ].  |(k * r) - l * proportional-round(r;k;l)| < l
BY
{ (Auto
   THEN (RW assert_pushupC 0 THENA Auto)
   THEN ((ElimOneRational⋅ THENA Auto)
         THEN ThinVar `r'
         THEN RepUR ``q_less proportional-round qdiv qabs qinv qmul qsub qadd qeq qpositive`` 0⋅
         THEN (RepeatFor 5 (Progress (CallByValueReduceOnTypes [⌜ℕ+⌝;⌜ℤ⌝;⌜ℤ × ℤ⌝]  0) THEN Reduce 0 THENA Auto)⋅
               THEN (CallByValueReduceOn ⌜<k * p * 1, q>⌝ 0⋅ THENA Auto)
               THEN (Subst ⌜isint(((p * 1) * k) ÷ q * l) ~ tt⌝ 0⋅ THENA Auto)
               THEN Reduce 0
               THEN (Subst ⌜isint(l * (((p * 1) * k) ÷ q * l)) ~ tt⌝ 0⋅ THENA Auto)
               THEN Reduce 0
               THEN (Progress (CallByValueReduceOnTypes [⌜ℕ+⌝;⌜ℤ⌝;⌜ℤ × ℤ⌝]  0) THEN Reduce 0 THENA Auto)⋅
               THEN (Subst ⌜isint((-1) * l * (((p * 1) * k) ÷ q * l)) ~ tt⌝ 0⋅ THENA Auto)
               THEN Reduce 0
               THEN (RepeatFor 2 (Progress (CallByValueReduceOnTypes [⌜ℕ+⌝;⌜ℤ⌝;⌜ℤ × ℤ⌝]  0) THEN Reduce 0 THENA Auto)⋅
                     THEN Repeat (AutoSplit)
                     THEN (RW assert_pushdownC 0 THENA Auto))⋅)⋅)⋅) }

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

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

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

---

Latex:

---

Latex:
\mforall{}[k,l:\mBbbN{}\msupplus{}].  \mforall{}[r:\mBbbQ{}].    |(k  *  r)  -  l  *  proportional-round(r;k;l)|  <  l


By

---

Latex:
(Auto
  THEN  (RW  assert\_pushupC  0  THENA  Auto)
  THEN  ((ElimOneRational\mcdot{}  THENA  Auto)
              THEN  ThinVar  `r'
              THEN  RepUR  ``q\_less  proportional-round  qdiv  qabs  qinv  qmul  qsub  qadd  qeq  qpositive``  0\mcdot{}
              THEN  (RepeatFor  5  (Progress  (CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbN{}\msupplus{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}  \mtimes{}  \mBbbZ{}\mkleeneclose{}
                          ]    0)  THEN  Reduce  0  THENA  Auto)\mcdot{}
                          THEN  (CallByValueReduceOn  \mkleeneopen{}<k  *  p  *  1,  q>\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                          THEN  (Subst  \mkleeneopen{}isint(((p  *  1)  *  k)  \mdiv{}  q  *  l)  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                          THEN  Reduce  0
                          THEN  (Subst  \mkleeneopen{}isint(l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                          THEN  Reduce  0
                          THEN  (Progress  (CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbN{}\msupplus{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}  \mtimes{}  \mBbbZ{}\mkleeneclose{}
                          ]    0)  THEN  Reduce  0  THENA  Auto)\mcdot{}
                          THEN  (Subst  \mkleeneopen{}isint((-1)  *  l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  \msim{}  tt\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                          THEN  Reduce  0
                          THEN  (RepeatFor  2  (Progress  (CallByValueReduceOnTypes  [\mkleeneopen{}\mBbbN{}\msupplus{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mBbbZ{}  \mtimes{}  \mBbbZ{}\mkleeneclose{}
                                      ]    0)  THEN  Reduce  0  THENA  Auto)\mcdot{}
                                      THEN  Repeat  (AutoSplit)
                                      THEN  (RW  assert\_pushdownC  0  THENA  Auto))\mcdot{})\mcdot{})\mcdot{})

---

Home Index