---

Step * 3 1 of Lemma proportional-round-property


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
BY
{ TACTIC:(Decide ⌜0 ≤ v⌝⋅ 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)) ∈ ℤ
12. 0 ≤ v
⊢ (¬v rem l * q < 0) ⇒ (-1) * (v rem l * q) < l * q

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. v : ℤ
10. (k * p) = v ∈ ℤ
11. v = (((v ÷ l * q) * l * q) + (v rem l * q)) ∈ ℤ
12. ¬(0 ≤ v)
⊢ (¬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{}0  <  (k  *  p  *  1)  +  (((-1)  *  l  *  (((p  *  1)  *  k)  \mdiv{}  q  *  l))  *  q)
6.  0  <  q
7.  \mneg{}(q  =  0)
8.  \mneg{}\muparrow{}qeq(q;0)
9.  v  :  \mBbbZ{}
10.  (k  *  p)  =  v
11.  v  =  (((v  \mdiv{}  l  *  q)  *  l  *  q)  +  (v  rem  l  *  q))
\mvdash{}  (\mneg{}v  rem  l  *  q  <  0)  {}\mRightarrow{}  (-1)  *  (v  rem  l  *  q)  <  l  *  q


By

---

Latex:
TACTIC:(Decide  \mkleeneopen{}0  \mleq{}  v\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index