---

Step * 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
⊢ k * p rem q < q
BY
{ (Decide ⌜0 ≤ p⌝⋅ THENA Auto) }

1
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

2
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

---

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


By

---

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

---

Home Index