---

Step * of Lemma rroot-abs-non-neg

∀i:{2...}. ∀x:ℝ. ∀n:ℕ+.  (0 ≤ (rroot-abs(i;x) n))
BY
{ (Auto
   THEN (RepUR ``rroot-abs`` 0 THEN (RW (AddrC [2;1;1] (RevLemmaC `exp-fastexp`)) 0 THENA Auto))
   THEN (GenConcl ⌜2^i - 1 = b ∈ ℕ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN (GenConcl ⌜n^i = k ∈ ℕ+⌝⋅
         THENA (Auto THEN (InstLemma `exp_preserves_lt` [⌜i⌝;⌜0⌝;⌜n⌝]⋅ THENA Auto) THEN RWO "exp-zero" (-1) THEN Auto)
         )
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (0  \mleq{}  (rroot-abs(i;x)  n))


By

---

Latex:
(Auto
  THEN  (RepUR  ``rroot-abs``  0  THEN  (RW  (AddrC  [2;1;1]  (RevLemmaC  `exp-fastexp`))  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}2\^{}i  -  1  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}n\^{}i  =  k\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  RWO  "exp-zero"  (-1)
                            THEN  Auto)
              )
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Auto)

---

Home Index