---

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


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))
BY
{ ((RW DivRemC 0 THENA Auto) THEN GenRem  THEN Auto) }

1
1. k : {2...}
2. x : ℝ
3. n : ℕ+
4. r : {r:ℤ| |r| < |2 * n|} 
5. ((x n) * (reg-seq-nexp(x;k - 1) n) rem 2 * n) = r ∈ {r:ℤ| |r| < |2 * n|} 
⊢ |((2 * n) * (reg-seq-nexp(x;k) n)) - ((x n) * (reg-seq-nexp(x;k - 1) n)) - r| ≤ ((|2 * n| * canonical-bound(x))
  + (|2 * n| * 6))

---

Latex:

---

Latex:

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


By

---

Latex:
((RW  DivRemC  0  THENA  Auto)  THEN  GenRem    THEN  Auto)

---

Home Index