---

Step * 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)
⊢ |(iroot(i;b * |x k|)^i ÷ 2 * n^i - 1) - |x n|| ≤ ((i * b * C^(i - 1)) + 5)
BY
{ (Assert |(n * |x k|) - k * |x n|| ≤ (2 * (k + n)) BY
         ((Assert regular-seq(|x|) BY
                 ((GenConclTerm ⌜|x|⌝⋅ THENA Auto) THEN D -2 THEN Unhide THEN Auto))
          THEN Unfold `regular-int-seq` -1
          THEN (InstHyp [⌜k⌝;⌜n⌝] (-1)⋅ THENA Auto)
          THEN (RWO "rabs-approx" (-1) THENA Auto)
          THEN Auto)) }

1
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)

---

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)
\mvdash{}  |(iroot(i;b  *  |x  k|)\^{}i  \mdiv{}  2  *  n\^{}i  -  1)  -  |x  n||  \mleq{}  ((i  *  b  *  C\^{}(i  -  1))  +  5)


By

---

Latex:
(Assert  |(n  *  |x  k|)  -  k  *  |x  n||  \mleq{}  (2  *  (k  +  n))  BY
              ((Assert  regular-seq(|x|)  BY
                              ((GenConclTerm  \mkleeneopen{}|x|\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Unhide  THEN  Auto))
                THEN  Unfold  `regular-int-seq`  -1
                THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                THEN  (RWO  "rabs-approx"  (-1)  THENA  Auto)
                THEN  Auto))

---

Home Index