---

Step * 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))
⊢ ∀n:ℕ+. (|(reg-seq-nexp(rroot-abs(i;x);i) n) - |x| n| ≤ ((i * 2^(i - 1) * C^(i - 1)) + 5))
BY
{ (ParallelLast
   THEN MoveToConcl (-1)
   THEN (RWO "rabs-approx" 0 THENA Auto)
   THEN Unfold `rroot-abs` 0
   THEN (Subst' 2^i - 1 ~ 2^(i - 1) 0 THENA Auto)
   THEN (GenConcl ⌜2^(i - 1) = b ∈ ℕ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepUR ``reg-seq-nexp`` 0
   THEN (GenConcl ⌜n^i = k ∈ ℕ+⌝⋅
         THENA (Auto THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜n⌝]⋅ THENA Auto) THEN RWO "exp-zero" (-1) THEN Auto)
         )
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN RWO "rabs-approx" 0
   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)
⊢ |(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))
\mvdash{}  \mforall{}n:\mBbbN{}\msupplus{}.  (|(reg-seq-nexp(rroot-abs(i;x);i)  n)  -  |x|  n|  \mleq{}  ((i  *  2\^{}(i  -  1)  *  C\^{}(i  -  1))  +  5))


By

---

Latex:
(ParallelLast
  THEN  MoveToConcl  (-1)
  THEN  (RWO  "rabs-approx"  0  THENA  Auto)
  THEN  Unfold  `rroot-abs`  0
  THEN  (Subst'  2\^{}i  -  1  \msim{}  2\^{}(i  -  1)  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}2\^{}(i  -  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepUR  ``reg-seq-nexp``  0
  THEN  (GenConcl  \mkleeneopen{}n\^{}i  =  k\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RWO  "exp-zero"  (-1)
                            THEN  Auto)
              )
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  RWO  "rabs-approx"  0
  THEN  Auto)

---

Home Index