---

Step * 1 1 of Lemma r-archimedean-implies


1. x : ℝ
2. m : ℕ+
3. n : ℕ
4. r(-n) ≤ (r(m) * x)
5. (r(m) * x) ≤ r(n)
⊢ ((r1/r(n + 1)) * x) ≤ (r1/r(m))
BY
{ ((Assert r(n) ≤ r(n + 1) BY
          Auto)
   THEN (Assert (r(m) * x) ≤ r(n + 1) BY
               Auto)
   THEN (Assert r0 < r(n + 1) BY
               Auto)
   THEN (Assert r0 < r(m) BY
               Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜r(n + 1)⌝;⌜r(m)⌝]⋅
   THEN All Thin) }

1
1. x : ℝ
2. v : ℝ
3. v1 : ℝ
⊢ ((v1 * x) ≤ v) ⇒ (r0 < v) ⇒ (r0 < v1) ⇒ (((r1/v) * x) ≤ (r1/v1))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  m  :  \mBbbN{}\msupplus{}
3.  n  :  \mBbbN{}
4.  r(-n)  \mleq{}  (r(m)  *  x)
5.  (r(m)  *  x)  \mleq{}  r(n)
\mvdash{}  ((r1/r(n  +  1))  *  x)  \mleq{}  (r1/r(m))


By

---

Latex:
((Assert  r(n)  \mleq{}  r(n  +  1)  BY
                Auto)
  THEN  (Assert  (r(m)  *  x)  \mleq{}  r(n  +  1)  BY
                          Auto)
  THEN  (Assert  r0  <  r(n  +  1)  BY
                          Auto)
  THEN  (Assert  r0  <  r(m)  BY
                          Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}r(n  +  1)\mkleeneclose{};\mkleeneopen{}r(m)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index