---

Step * 2 of Lemma rnexp-req


1. k : {1...}
2. k - 1 ≠ 0
3. k ≠ 0
4. x : ℝ
⊢ bdd-diff(accelerate((k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1;reg-seq-nexp(x;k));reg-seq-mul(x;accelerate(((k 
           - 1)
           * ((canon-bnd(x)^k - 1 - 1 ÷ 2^k - 1 - 1) + 1))
           + 1;reg-seq-nexp(x;k - 1))))
BY
{ ((Assert ⌜k ≠ 1⌝⋅ THENA Auto)
   THEN (CombineNequalWithLe THENA Auto)
   THEN RepeatFor 2 (Thin (-2))
   THEN (RWO "exp-fastexp<" 0 THENA Auto)) }

1
1. k : {2...}
2. x : ℝ
⊢ bdd-diff(accelerate((k * ((canon-bnd(x)^(k - 1) ÷ 2^(k - 1)) + 1)) + 1;reg-seq-nexp(x;k));
           reg-seq-mul(x;accelerate(((k - 1) * ((canon-bnd(x)^(k - 1 - 1) ÷ 2^(k - 1 - 1)) + 1)) + 1;reg-seq-nexp(x;k 
           - 1))))

---

Latex:

---

Latex:

1.  k  :  \{1...\}
2.  k  -  1  \mneq{}  0
3.  k  \mneq{}  0
4.  x  :  \mBbbR{}
\mvdash{}  bdd-diff(accelerate((k  *  ((canon-bnd(x)\^{}k  -  1  \mdiv{}  2\^{}k  -  1)  +  1))  +  1;reg-seq-nexp(x;k));
                      reg-seq-mul(x;accelerate(((k  -  1)  *  ((canon-bnd(x)\^{}k  -  1  -  1  \mdiv{}  2\^{}k  -  1  -  1)  +  1))
                      +  1;reg-seq-nexp(x;k  -  1))))


By

---

Latex:
((Assert  \mkleeneopen{}k  \mneq{}  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CombineNequalWithLe  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  (RWO  "exp-fastexp<"  0  THENA  Auto))

---

Home Index