---

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


1. k : {2...}
2. x : ℝ
⊢ bdd-diff(reg-seq-nexp(x;k);reg-seq-mul(x;reg-seq-nexp(x;k - 1)))
BY
{ (With ⌜canonical-bound(x) + 6⌝ (D 0)⋅ THEN Auto) }

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

---

Latex:

---

Latex:

1.  k  :  \{2...\}
2.  x  :  \mBbbR{}
\mvdash{}  bdd-diff(reg-seq-nexp(x;k);reg-seq-mul(x;reg-seq-nexp(x;k  -  1)))


By

---

Latex:
(With  \mkleeneopen{}canonical-bound(x)  +  6\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index