---

Step * 1 1 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 rem q
8. 0 ≤ p
⊢ k * p rem q < q
BY
{ (InstLemma `rem_bounds_1` [⌜k * p⌝;⌜q⌝]⋅ THEN Auto)⋅ }

---

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  rem  q
8.  0  \mleq{}  p
\mvdash{}  k  *  p  rem  q  <  q


By

---

Latex:
(InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}k  *  p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index