---

Step * 1 of Lemma integer-nth-root

.....antecedent..... 
1. n : ℕ+
2. b : {b:ℤ| 1 < b} 
3. b = 2^n ∈ {b:ℤ| 1 < b} 
⊢ ∃r:ℕ [((r^n ≤ 0) ∧ 0 < (r + 1)^n)]
BY
{ With ⌜0⌝ (D 0)⋅
THEN (Reduce 0 THEN Auto THEN RWO  "exp-zero exp-one" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
3.  b  =  2\^{}n
\mvdash{}  \mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  0)  \mwedge{}  0  <  (r  +  1)\^{}n)]


By

---

Latex:
With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}
THEN  (Reduce  0  THEN  Auto  THEN  RWO    "exp-zero  exp-one"  0  THEN  Auto)\mcdot{}

---

Home Index