---

Step * 2 of Lemma integer-nth-root


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)]
BY
{ (D -1
   THEN (Evaluate ⌜r2 = (2 * r) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜r2' = (r2 + 1) ∈ ℤ⌝⋅ THENA Auto)
   THEN (InstLemma `exp-of-mul` [⌜2⌝;⌜r⌝;⌜n⌝]⋅ THENA Auto)
   THEN (InstLemma `exp-of-mul` [⌜2⌝;⌜r + 1⌝;⌜n⌝]⋅ THENA Auto)
   THEN ((InstLemma `div_rem_sum` [⌜i⌝; ⌜2^n⌝])⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜i⌝; ⌜2^n⌝])⋅
   THEN Auto
   THEN ((Decide ⌜r2'^n < i + 1⌝⋅ THENA Auto) THEN All (RWO "exp-fastexp<") THEN Auto)) }

1
1. n : ℕ+
2. b : {b:ℤ| 1 < b} 
3. b = 2^n ∈ {b:ℤ| 1 < b} 
4. i : ℕ+
5. r : ℕ
6. [%6] : (r^n ≤ (i ÷ b)) ∧ i ÷ b < (r + 1)^n
7. r2 : ℤ
8. r2 = (2 * r) ∈ ℤ
9. r2' : ℤ
10. r2' = (r2 + 1) ∈ ℤ
11. (2 * r)^n = (2^n * r^n) ∈ ℤ
12. (2 * (r + 1))^n = (2^n * (r + 1)^n) ∈ ℤ
13. i = (((i ÷ 2^n) * 2^n) + (i rem 2^n)) ∈ ℤ
14. 0 ≤ (i rem 2^n)
15. i rem 2^n < 2^n
16. r2'^n < i + 1
⊢ ∃r:ℕ [((r^n ≤ i) ∧ i < (r + 1)^n)]

2
1. n : ℕ+
2. b : {b:ℤ| 1 < b} 
3. b = 2^n ∈ {b:ℤ| 1 < b} 
4. i : ℕ+
5. r : ℕ
6. [%6] : (r^n ≤ (i ÷ b)) ∧ i ÷ b < (r + 1)^n
7. r2 : ℤ
8. r2 = (2 * r) ∈ ℤ
9. r2' : ℤ
10. r2' = (r2 + 1) ∈ ℤ
11. (2 * r)^n = (2^n * r^n) ∈ ℤ
12. (2 * (r + 1))^n = (2^n * (r + 1)^n) ∈ ℤ
13. i = (((i ÷ 2^n) * 2^n) + (i rem 2^n)) ∈ ℤ
14. 0 ≤ (i rem 2^n)
15. i rem 2^n < 2^n
16. ¬r2'^n < i + 1
⊢ ∃r:ℕ [((r^n ≤ i) ∧ i < (r + 1)^n)]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
3.  b  =  2\^{}n
4.  i  :  \mBbbN{}\msupplus{}
5.  \mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  (i  \mdiv{}  b))  \mwedge{}  i  \mdiv{}  b  <  (r  +  1)\^{}n)]
\mvdash{}  \mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  i)  \mwedge{}  i  <  (r  +  1)\^{}n)]


By

---

Latex:
(D  -1
  THEN  (Evaluate  \mkleeneopen{}r2  =  (2  *  r)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}r2'  =  (r2  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `exp-of-mul`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `exp-of-mul`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}r  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}2\^{}n\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}2\^{}n\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  ((Decide  \mkleeneopen{}r2'\^{}n  <  i  +  1\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  (RWO  "exp-fastexp<")  THEN  Auto))

---

Home Index