---

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
{ (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:
(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