---

Step * of Lemma rroot-odd_wf

∀i:{2...}. ∀x:ℝ.  (rroot-odd(i;x) ∈ ℕ+ ⟶ ℤ)
BY
{ (Auto
   THEN Unfold `rroot-odd` 0
   THEN (RW (AddrC [2;1] (RevLemmaC `exp-fastexp`)) 0 THENA Auto)
   THEN (GenConcl ⌜2^i - 1 = b ∈ ℕ⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (MemCD THENA Auto)
   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{}.    (rroot-odd(i;x)  \mmember{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})


By

---

Latex:
(Auto
  THEN  Unfold  `rroot-odd`  0
  THEN  (RW  (AddrC  [2;1]  (RevLemmaC  `exp-fastexp`))  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}2\^{}i  -  1  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (MemCD  THENA  Auto)
  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