---

Step * 1 of Lemma q-archimedean


1. a : ℚ
2. p : ℤ
3. q : ℤ
4. 0 < q
5. ¬(q = 0 ∈ ℚ)
6. a = (p/q) ∈ ℚ
7. ¬↑qeq(q;0)
8. p = (((p ÷ q) * q) + (p rem q)) ∈ ℤ
9. 0 < q
10. 0 ≤ p
11. (0 ≤ (p rem q)) ∧ p rem q < q
12. 0 ≤ (p ÷ q)
⊢ ∃n:ℕ. ((-(n) ≤ (p/q)) ∧ ((p/q) ≤ n))
BY
{ ((With ⌜(p ÷ q) + 1⌝ (D 0)⋅ THEN Auto)⋅
   THEN QMul ⌜q⌝ 0⋅
   THEN Auto
   THEN RepeatFor 2 ((RWW "qmul-mul" 0 THEN Auto))⋅
   THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((With  \mkleeneopen{}(p  \mdiv{}  q)  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}
  THEN  QMul  \mkleeneopen{}q\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((RWW  "qmul-mul"  0  THEN  Auto))\mcdot{}
  THEN  Auto')

---

Home Index