---

Step * 1 1 of Lemma fractional-part-rep


1. r : ℚ
2. 0 ≤ r
3. r < 1
4. p : ℤ
5. q : ℤ
6. 0 < q
7. ¬(q = 0 ∈ ℚ)
8. r = (p/q) ∈ ℚ
9. ¬↑qeq(q;0)
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))
BY
{ (xxx(Assert (0 ≤ r) ∧ r < 1 BY Auto)xxx THEN ElimVar `r' THEN Auto THEN ThinVar `r' THEN (Decide 0 ≤ q THENA Auto)) }

1
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
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))

2
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)
⊢ ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ ((p/q) = (a/b) ∈ ℚ))

---

Latex:

---

Latex:

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


By

---

Latex:
(xxx(Assert  (0  \mleq{}  r)  \mwedge{}  r  <  1  BY
                      Auto)xxx
  THEN  ElimVar  `r'
  THEN  Auto
  THEN  ThinVar  `r'
  THEN  (Decide  0  \mleq{}  q  THENA  Auto))

---

Home Index