---

Step * 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))
⊢ bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)
BY
{ (With ⌜(i * 2^(i - 1) * C^(i - 1)) + 5⌝ (D 0)⋅ THENA Auto) }

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

---

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{}  bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)


By

---

Latex:
(With  \mkleeneopen{}(i  *  2\^{}(i  -  1)  *  C\^{}(i  -  1))  +  5\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)

---

Home Index