---

Step * 1 1 1 1 1 of Lemma rroot-abs-property


1. i : {2...}
2. i ≠ 0
3. x : ℝ
4. C : {2...}
5. ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * C))
6. n : ℕ+
7. b : ℕ
8. 2^(i - 1) = b ∈ ℕ
9. k : ℕ+
10. n^i = k ∈ ℕ+
11. |iroot(i;b * |x k|)| ≤ ((2 * n) * C)
12. |(n * |x k|) - k * |x n|| ≤ (2 * (k + n))
⊢ |(iroot(i;b * |x k|)^i ÷ 2 * n^i - 1) - |x n|| ≤ ((i * b * C^(i - 1)) + 5)
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜|x k|⌝;⌜|x n|⌝]⋅
   THEN RenameVar `A' (-4)
   THEN RenameVar `B' (-2)
   THEN Auto
   THEN ThinVar `x') }

1
1. i : {2...}
2. i ≠ 0
3. C : {2...}
4. n : ℕ+
5. b : ℕ
6. 2^(i - 1) = b ∈ ℕ
7. k : ℕ+
8. n^i = k ∈ ℕ+
9. A : ℕ
10. B : ℕ
11. |iroot(i;b * A)| ≤ ((2 * n) * C)
12. |(n * A) - k * B| ≤ (2 * (k + n))
⊢ |(iroot(i;b * A)^i ÷ 2 * n^i - 1) - B| ≤ ((i * b * C^(i - 1)) + 5)

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  i  \mneq{}  0
3.  x  :  \mBbbR{}
4.  C  :  \{2...\}
5.  \mforall{}n:\mBbbN{}\msupplus{}.  (|rroot-abs(i;x)  n|  \mleq{}  ((2  *  n)  *  C))
6.  n  :  \mBbbN{}\msupplus{}
7.  b  :  \mBbbN{}
8.  2\^{}(i  -  1)  =  b
9.  k  :  \mBbbN{}\msupplus{}
10.  n\^{}i  =  k
11.  |iroot(i;b  *  |x  k|)|  \mleq{}  ((2  *  n)  *  C)
12.  |(n  *  |x  k|)  -  k  *  |x  n||  \mleq{}  (2  *  (k  +  n))
\mvdash{}  |(iroot(i;b  *  |x  k|)\^{}i  \mdiv{}  2  *  n\^{}i  -  1)  -  |x  n||  \mleq{}  ((i  *  b  *  C\^{}(i  -  1))  +  5)


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}|x  k|\mkleeneclose{};\mkleeneopen{}|x  n|\mkleeneclose{}]\mcdot{}
  THEN  RenameVar  `A'  (-4)
  THEN  RenameVar  `B'  (-2)
  THEN  Auto
  THEN  ThinVar  `x')

---

Home Index