---

Step * 1 2 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) + ((-1) * q * ((k * p) ÷ q)) < 0
⊢ ((-1) * k * p) + (q * ((k * p) ÷ q)) < q
BY
{ (MoveToConcl (-1)
   THEN (Subst' q * ((k * p) ÷ q) ~ (k * p) - k * p rem q 0 THENA (InstLemma `div_rem_sum` [⌜k * p⌝;⌜q⌝]⋅ THEN Auto'))
   THEN RW IntNormC 0
   THEN 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
⊢ (-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)  +  ((-1)  *  q  *  ((k  *  p)  \mdiv{}  q))  <  0
\mvdash{}  ((-1)  *  k  *  p)  +  (q  *  ((k  *  p)  \mdiv{}  q))  <  q


By

---

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

---

Home Index