---

Step * 1 of Lemma rroot-abs-property


1. i : {2...}
2. i ≠ 0
3. x : ℝ
4. v : {k:{2...}| ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * k))} 
5. canonical-bound(rroot-abs(i;x)) = v ∈ {k:{2...}| ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * k))} 
⊢ bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)
BY
{ (Thin (-1)
   THEN RenameVar `C' (-1)
   THEN (Assert ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * C)) BY
               (D -1 THEN Auto))
   THEN D -2
   THEN Thin (-2)) }

1
1. i : {2...}
2. i ≠ 0
3. x : ℝ
4. C : {2...}
5. ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * C))
⊢ bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)

---

Latex:

---

Latex:

1.  i  :  \{2...\}
2.  i  \mneq{}  0
3.  x  :  \mBbbR{}
4.  v  :  \{k:\{2...\}|  \mforall{}n:\mBbbN{}\msupplus{}.  (|rroot-abs(i;x)  n|  \mleq{}  ((2  *  n)  *  k))\} 
5.  canonical-bound(rroot-abs(i;x))  =  v
\mvdash{}  bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)


By

---

Latex:
(Thin  (-1)
  THEN  RenameVar  `C'  (-1)
  THEN  (Assert  \mforall{}n:\mBbbN{}\msupplus{}.  (|rroot-abs(i;x)  n|  \mleq{}  ((2  *  n)  *  C))  BY
                          (D  -1  THEN  Auto))
  THEN  D  -2
  THEN  Thin  (-2))

---

Home Index