---

Step * of Lemma q-archimedean

∀a:ℚ. ∃n:ℕ. ((-(n) ≤ a) ∧ (a ≤ n))
BY
{ (Auto
   THEN ((BetterRationalD (-1)) THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜p⌝;⌜q⌝]⋅ THENA Auto)
   THEN (Assert 0 < q BY
               (RWO "qless-int" 0 THEN Auto))
   THEN ((Decide ⌜0 ≤ p⌝⋅ THENA Auto)
         THENL [((InstLemma `rem_bounds_1` [⌜p⌝;⌜q⌝]⋅ THENA Auto) THEN (InstLemma `div_bounds_1` [⌜p⌝;⌜q⌝]⋅ THENA Auto))
               ; ((InstLemma `rem_bounds_2` [⌜p⌝;⌜q⌝]⋅ THENA Auto)
                  THEN (InstLemma `div_bounds_2` [⌜p⌝;⌜q⌝]⋅ THENA Auto)
                  )]
   )) }

1
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))

2
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))

---

Latex:

---

Latex:
\mforall{}a:\mBbbQ{}.  \mexists{}n:\mBbbN{}.  ((-(n)  \mleq{}  a)  \mwedge{}  (a  \mleq{}  n))


By

---

Latex:
(Auto
  THEN  ((BetterRationalD  (-1))  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  0  <  q  BY
                          (RWO  "qless-int"  0  THEN  Auto))
  THEN  ((Decide  \mkleeneopen{}0  \mleq{}  p\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              )
                          ;  ((InstLemma  `rem\_bounds\_2`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  (InstLemma  `div\_bounds\_2`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                )]
  ))

---

Home Index