---

Step * 1 of Lemma integer-nth-root2


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))]
BY
{ TACTIC:(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') }

---

Latex:

---

Latex:

1.  n  :  \{n:\mBbbN{}\msupplus{}|  (n  mod  2)  =  1\}  @i
2.  x  :  \{...0\}@i
3.  \mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  (-x))  \mwedge{}  -x  <  (r  +  1)\^{}n)]
\mvdash{}  \mexists{}r:\{...0\}  [((r  -  1)\^{}n  <  x  \mwedge{}  (x  \mleq{}  r\^{}n))]


By

---

Latex:
TACTIC:(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