---

Step * 1 1 1 2 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_2` [⌜k * p⌝;⌜q⌝]⋅ THEN Auto THEN MemTypeCD 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.  \mneg{}(0  \mleq{}  p)
\mvdash{}  k  *  p  rem  q  <  q


By

---

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

---

Home Index