---

Step * of Lemma r-archimedean-implies2

∀x:ℝ. ∀d:{d:ℝ| r0 < d} .  ∃M:ℕ+. ((x/r(M)) ≤ d)
BY
{ (Auto
   THEN (InstLemma `small-reciprocal-real` [⌜d⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstLemma `r-archimedean-implies` [⌜x⌝;⌜k⌝]⋅ THENA Auto)
   THEN ParallelLast) }

1
1. x : ℝ
2. d : {d:ℝ| r0 < d} 
3. k : ℕ+
4. (r1/r(k)) < d
5. M : ℕ+
6. ((r1/r(M)) * x) ≤ (r1/r(k))
⊢ (x/r(M)) ≤ d

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}d:\{d:\mBbbR{}|  r0  <  d\}  .    \mexists{}M:\mBbbN{}\msupplus{}.  ((x/r(M))  \mleq{}  d)


By

---

Latex:
(Auto
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `r-archimedean-implies`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast)

---

Home Index