---

Step * of Lemma integer-nth-root2

∀n:{n:ℕ+| (n mod 2) = 1 ∈ ℤ} . ∀x:{...0}.  (∃r:{...0} [((r - 1)^n < x ∧ (x ≤ r^n))])
BY
{ (Auto
   THEN (InstLemma `integer-nth-root-ext` [⌜n⌝;⌜-x⌝]⋅ THENA Auto)
   THEN skip{(D -1
              THEN With ⌜-r⌝ (D 0)⋅
              THEN Auto
              THEN (Subst' (-r) - 1 ~ -(r + 1) 0 THENA Auto)
              THEN (RWO "exp-minus" 0 THENA Auto)
              THEN (Subst' n mod 2 ~ 1 0 THENA Auto)
              THEN Reduce 0
              THEN Auto')}) }

1
1. n : {n:ℕ+| (n mod 2) = 1 ∈ ℤ} @i
2. x : {...0}@i
3. ∃r:ℕ [((r^n ≤ (-x)) ∧ -x < (r + 1)^n)]
⊢ ∃r:{...0} [((r - 1)^n < x ∧ (x ≤ r^n))]

---

Latex:

---

Latex:
\mforall{}n:\{n:\mBbbN{}\msupplus{}|  (n  mod  2)  =  1\}  .  \mforall{}x:\{...0\}.    (\mexists{}r:\{...0\}  [((r  -  1)\^{}n  <  x  \mwedge{}  (x  \mleq{}  r\^{}n))])


By

---

Latex:
(Auto
  THEN  (InstLemma  `integer-nth-root-ext`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}-x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  skip\{(D  -1
                        THEN  With  \mkleeneopen{}-r\mkleeneclose{}  (D  0)\mcdot{}
                        THEN  Auto
                        THEN  (Subst'  (-r)  -  1  \msim{}  -(r  +  1)  0  THENA  Auto)
                        THEN  (RWO  "exp-minus"  0  THENA  Auto)
                        THEN  (Subst'  n  mod  2  \msim{}  1  0  THENA  Auto)
                        THEN  Reduce  0
                        THEN  Auto')\})

---

Home Index