---

Step * 1 1 of Lemma proportional-round-property


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

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


By

---

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

---

Home Index