---

Step * 3 of Lemma proportional-round-property


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
BY
{ (MoveToConcl (-5)
   THEN (RW IntNormC 0 THENA Auto)
   THEN (GenConclTerm ⌜k * p⌝⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜v⌝;⌜l * q⌝]⋅ THENA Auto)
   THEN (Subst ⌜l * q * (v ÷ l * q) ~ v - v rem l * q⌝ 0⋅ THENA Auto')
   THEN (RW IntNormC 0 THENA Auto)⋅)⋅ }

1
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. v : ℤ
10. (k * p) = v ∈ ℤ
11. v = (((v ÷ l * q) * l * q) + (v rem l * q)) ∈ ℤ
⊢ (¬v rem l * q < 0) ⇒ (-1) * (v rem l * q) < l * q

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
2.  l  :  \mBbbN{}\msupplus{}
3.  p  :  \mBbbZ{}
4.  q  :  \mBbbZ{}
5.  \mneg{}(k  *  p  *  1)  +  (((-1)  *  l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  *  q)  <  0
6.  \mneg{}0  <  (k  *  p  *  1)  +  (((-1)  *  l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  *  q)
7.  0  <  q
8.  \mneg{}(q  =  0)
9.  \mneg{}\muparrow{}qeq(q;0)
\mvdash{}  (-1)  *  ((k  *  p  *  1)  +  (((-1)  *  l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  *  q))  <  q  *  l


By

---

Latex:
(MoveToConcl  (-5)
  THEN  (RW  IntNormC  0  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}k  *  p\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}l  *  q\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}l  *  q  *  (v  \mdiv{}  l  *  q)  \msim{}  v  -  v  rem  l  *  q\mkleeneclose{}  0\mcdot{}  THENA  Auto')
  THEN  (RW  IntNormC  0  THENA  Auto)\mcdot{})\mcdot{}

---

Home Index