---

Step * of Lemma integer-nth-root

∀n:ℕ+. ∀x:ℕ.  (∃r:ℕ [((r^n ≤ x) ∧ x < (r + 1)^n)])
BY
{ ((D 0 THENA Auto)
   THEN (Evaluate ⌜b = 2^n ∈ {b:ℤ| 1 < b} ⌝⋅ THENA (Auto THEN InstLemma `exp_preserves_lt` [⌜n⌝;⌜1⌝;⌜2⌝]⋅ THEN Auto))
   THEN InstLemma `div_nat_induction` [⌜b⌝;⌜λ2x.∃r:ℕ [((r^n ≤ x) ∧ x < (r + 1)^n)]⌝]⋅
   THEN Auto
   THEN Try ((RWO "exp-fastexp<" 0 THEN Auto)⋅)) }

1
.....antecedent..... 
1. n : ℕ+
2. b : {b:ℤ| 1 < b} 
3. b = 2^n ∈ {b:ℤ| 1 < b} 
⊢ ∃r:ℕ [((r^n ≤ 0) ∧ 0 < (r + 1)^n)]

2
1. n : ℕ+
2. b : {b:ℤ| 1 < b} 
3. b = 2^n ∈ {b:ℤ| 1 < b} 
4. i : ℕ+
5. ∃r:ℕ [((r^n ≤ (i ÷ b)) ∧ i ÷ b < (r + 1)^n)]
⊢ ∃r:ℕ [((r^n ≤ i) ∧ i < (r + 1)^n)]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbN{}.    (\mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)\^{}n)])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}b  =  2\^{}n\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  InstLemma  `exp\_preserves\_lt`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  InstLemma  `div\_nat\_induction`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.\mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)\^{}n)]\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "exp-fastexp<"  0  THEN  Auto)\mcdot{}))

---

Home Index