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