---

Step * 2 1 1 1 1 1 1 1 of Lemma rnexp-req


1. k : {2...}
2. x : ℝ
3. n : ℕ+
⊢ |(reg-seq-nexp(x;k) n) - reg-seq-mul(x;reg-seq-nexp(x;k - 1)) n| ≤ (canonical-bound(x) + 6)
BY
{ (RepUR ``reg-seq-mul`` 0 THEN (MulAbs ⌜2 * n⌝ 0⋅ THENA Auto)) }

1
1. k : {2...}
2. x : ℝ
3. n : ℕ+
⊢ |((2 * n) * (reg-seq-nexp(x;k) n)) - (2 * n) * (((x n) * (reg-seq-nexp(x;k - 1) n)) ÷ 2 * n)| ≤ ((|2 * n|
  * canonical-bound(x))
  + (|2 * n| * 6))

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  x  :  \mBbbR{}
3.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  |(reg-seq-nexp(x;k)  n)  -  reg-seq-mul(x;reg-seq-nexp(x;k  -  1))  n|  \mleq{}  (canonical-bound(x)  +  6)


By

---

Latex:
(RepUR  ``reg-seq-mul``  0  THEN  (MulAbs  \mkleeneopen{}2  *  n\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index