---

Step * of Lemma rroot-abs-property

∀i:{2...}. ∀x:ℝ.  (rroot-abs(i;x)^i = |x|)
BY
{ ((Auto
    THEN (BLemma `req-iff-bdd-diff` THENA Auto)
    THEN Unfold `rnexp` 0
    THEN (CallByValueReduce 0 THENA Auto)
    THEN AutoSplit
    THEN (GenConclTerm ⌜canonical-bound(rroot-abs(i;x))⌝⋅ THENA Auto)
    THEN (CallByValueReduce 0 THENA Auto)
    THEN Fold `reg-seq-nexp` 0
    THEN (RWO "accelerate-bdd-diff" 0 THENA Auto))
   THEN Try (Complete (((RWO "exp-fastexp<" 0 THEN Auto)
                        THEN InstLemma `exp-positive` [⌜i - 1⌝;⌜v⌝]⋅
                        THEN Auto
                        THEN Mul ⌜i⌝ (-1)⋅
                        THEN Auto)))
   ) }

1
1. i : {2...}
2. i ≠ 0
3. x : ℝ
4. v : {k:{2...}| ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * k))} 
5. canonical-bound(rroot-abs(i;x)) = v ∈ {k:{2...}| ∀n:ℕ+. (|rroot-abs(i;x) n| ≤ ((2 * n) * k))} 
⊢ bdd-diff(reg-seq-nexp(rroot-abs(i;x);i);|x|)

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.    (rroot-abs(i;x)\^{}i  =  |x|)


By

---

Latex:
((Auto
    THEN  (BLemma  `req-iff-bdd-diff`  THENA  Auto)
    THEN  Unfold  `rnexp`  0
    THEN  (CallByValueReduce  0  THENA  Auto)
    THEN  AutoSplit
    THEN  (GenConclTerm  \mkleeneopen{}canonical-bound(rroot-abs(i;x))\mkleeneclose{}\mcdot{}  THENA  Auto)
    THEN  (CallByValueReduce  0  THENA  Auto)
    THEN  Fold  `reg-seq-nexp`  0
    THEN  (RWO  "accelerate-bdd-diff"  0  THENA  Auto))
  THEN  Try  (Complete  (((RWO  "exp-fastexp<"  0  THEN  Auto)
                                            THEN  InstLemma  `exp-positive`  [\mkleeneopen{}i  -  1\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
                                            THEN  Auto
                                            THEN  Mul  \mkleeneopen{}i\mkleeneclose{}  (-1)\mcdot{}
                                            THEN  Auto)))
  )

---

Home Index