---

Step * 1 of Lemma proportional-round-property


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
BY
{ (MoveToConcl (-3)
   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 < q
6. ¬(q = 0 ∈ ℚ)
7. 0 < (k * p * 1) + (((-1) * l * (((p * 1) * k) ÷ q * l)) * q)
8. 0 < q
9. v : ℤ@i
10. (k * p) = v ∈ ℤ
11. v = (((v ÷ l * q) * l * q) + (v rem l * q)) ∈ ℤ
⊢ (¬↑qeq(q;0)) ⇒ v rem l * q < l * q

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-3)
  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))

---

Home Index