---

Step * 1 1 of Lemma rounded-numerator-property


1. k : ℕ+
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
7. 0 < (k * p) + ((-1) * q * ((k * p) ÷ q))
⊢ (k * p) + ((-1) * 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 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
7. 0 < k * p rem q
⊢ k * p rem q < q

---

Latex:

---

Latex:

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