---

Step * of Lemma rnexp-req

∀[k:ℕ]. ∀[x:ℝ].  (x^k = if (k =z 0) then r1 else x * x^k - 1 fi )
BY
{ (Auto
   THEN AutoSplit
   THEN Try ((HypSubst' (-1) 0 THEN RepUR ``rnexp`` 0 THEN Auto)⋅)
   THEN (BLemma `req-iff-bdd-diff` THENA Auto)
   THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0 THENA Auto)
   THEN Unfold `rnexp` 0
   THEN Fold `reg-seq-nexp` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoSplit
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoSplit) }

1
1. k : {1...}
2. k ≠ 0
3. x : ℝ
4. (k - 1) = 0 ∈ ℤ
⊢ bdd-diff(accelerate((k * ((canon-bnd(x)^k - 1 ÷ 2^k - 1) + 1)) + 1;reg-seq-nexp(x;k));reg-seq-mul(x;r1))

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbR{}].    (x\^{}k  =  if  (k  =\msubz{}  0)  then  r1  else  x  *  x\^{}k  -  1  fi  )


By

---

Latex:
(Auto
  THEN  AutoSplit
  THEN  Try  ((HypSubst'  (-1)  0  THEN  RepUR  ``rnexp``  0  THEN  Auto)\mcdot{})
  THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
  THEN  (RWO  "rmul-bdd-diff-reg-seq-mul"  0  THENA  Auto)
  THEN  Unfold  `rnexp`  0
  THEN  Fold  `reg-seq-nexp`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index