---

Step * of Lemma approx-root-property

∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+.
  ((0 ≤ a ⇐⇒ 0 ≤ k-th root(a) within 1/n) ∧ |k-th root(a) within 1/n ↑ k - a| < (1/n))
BY
{ ((UnivCD⋅ THENA Auto)
   THEN Unfold `approx-root` 0
   THEN (GenConclAtAddr [1;2;2] THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\{2...\}.  \mforall{}a:\{a:\mBbbQ{}|  (0  \mleq{}  a)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    ((0  \mleq{}  a  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  k-th  root(a)  within  1/n)  \mwedge{}  |k-th  root(a)  within  1/n  \muparrow{}  k  -  a|  <  (1/n))


By

---

Latex:
((UnivCD\mcdot{}  THENA  Auto)
  THEN  Unfold  `approx-root`  0
  THEN  (GenConclAtAddr  [1;2;2]  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Unhide
  THEN  Auto)

---

Home Index