---

Step * 1 2 1 of Lemma rounded-numerator-property


1. k : ℕ+
2. p : ℤ
3. q : ℤ
4. ¬0 < (k * p) + ((-1) * q * ((k * p) ÷ q))
5. 0 < q
6. ¬(q = 0 ∈ ℚ)
7. ¬↑qeq(q;0)
8. k * p rem q < 0
⊢ (-1) * (k * p rem q) < q
BY
{ (Decide ⌜0 ≤ p⌝⋅ THENA Auto)⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index