---

Step * 1 1 2 2 1 1 of Lemma fractional-part-rep


1. p : ℤ
2. q : ℤ
3. (p/q) ∈ ℚ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
7. 0 ≤ (-p/-q)
8. (-p/-q) < 1
9. ¬(0 ≤ q)
10. (p/q) = (-p/-q) ∈ ℚ
11. ¬((-q) = 0 ∈ ℚ)
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))
BY
{ ((QMul ⌜-q⌝ (-5)⋅ THENA Auto) THEN (QMul ⌜-q⌝ (-4)⋅ THENA Auto))⋅ }

1
1. p : ℤ
2. q : ℤ
3. (p/q) ∈ ℚ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. ¬↑qeq(q;0)
7. 0 ≤ (-p)
8. -p < -q
9. ¬(0 ≤ q)
10. (p/q) = (-p/-q) ∈ ℚ
11. ¬((-q) = 0 ∈ ℚ)
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}
2.  q  :  \mBbbZ{}
3.  (p/q)  \mmember{}  \mBbbQ{}
4.  0  <  q
5.  \mneg{}(q  =  0)
6.  \mneg{}\muparrow{}qeq(q;0)
7.  0  \mleq{}  (-p/-q)
8.  (-p/-q)  <  1
9.  \mneg{}(0  \mleq{}  q)
10.  (p/q)  =  (-p/-q)
11.  \mneg{}((-q)  =  0)
\mvdash{}  \mexists{}a,b:\mBbbN{}.  ((0  \mleq{}  a)  \mwedge{}  a  <  b  \mwedge{}  ((p/q)  =  (a/b)))


By

---

Latex:
((QMul  \mkleeneopen{}-q\mkleeneclose{}  (-5)\mcdot{}  THENA  Auto)  THEN  (QMul  \mkleeneopen{}-q\mkleeneclose{}  (-4)\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index