---

Step * of Lemma small-reciprocal-real

∀x:{x:ℝ| r0 < x} . ∃k:ℕ+. ((r1/r(k)) < x)
BY
{ (Auto
   THEN ((Evaluate ⌜n = rlessw(r0;x) ∈ {n:ℕ+| (r0 n) + 4 < x n} ⌝⋅ THENA Auto) THEN Thin (-1))
   THEN (Assert 4 < x n BY
               (D -1 THEN (Unhide THENA Auto) THEN RepUR ``int-to-real`` (-1) THEN Auto'))
   THEN D (-2)
   THEN Thin (-2)
   THEN (InstLemma `rational-approx-property2` [⌜x⌝;⌜n⌝]⋅ THENA Auto)
   THEN RepUR ``rational-approx`` (-1)
   THEN (With ⌜n + 1⌝ (D 0)⋅ THENA Auto)) }

1
1. x : {x:ℝ| r0 < x} 
2. n : ℕ+
3. 4 < x n
4. ((r(x n))/2 * n - (r1/r(n))) ≤ x
⊢ (r1/r(n + 1)) < x

---

Latex:

---

Latex:
\mforall{}x:\{x:\mBbbR{}|  r0  <  x\}  .  \mexists{}k:\mBbbN{}\msupplus{}.  ((r1/r(k))  <  x)


By

---

Latex:
(Auto
  THEN  ((Evaluate  \mkleeneopen{}n  =  rlessw(r0;x)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1))
  THEN  (Assert  4  <  x  n  BY
                          (D  -1  THEN  (Unhide  THENA  Auto)  THEN  RepUR  ``int-to-real``  (-1)  THEN  Auto'))
  THEN  D  (-2)
  THEN  Thin  (-2)
  THEN  (InstLemma  `rational-approx-property2`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``rational-approx``  (-1)
  THEN  (With  \mkleeneopen{}n  +  1\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))

---

Home Index