---

Step * 2 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. (p ÷ q) ≤ 0
⊢ ∃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.  \mneg{}(0  \mleq{}  p)
11.  (0  \mgeq{}  (p  rem  q)  )  \mwedge{}  ((p  rem  q)  >  (-q))
12.  (p  \mdiv{}  q)  \mleq{}  0
\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))
  THEN  Auto')

---

Home Index