---

Step * 2 2 of Lemma integer-nth-root


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)]
BY
{ (With ⌜r2⌝ (D 0)⋅ THEN Auto' THEN ElimVar `r2\'' THEN ElimVar `r2' THEN Auto')⋅ }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
3.  b  =  2\^{}n
4.  i  :  \mBbbN{}\msupplus{}
5.  r  :  \mBbbN{}
6.  [\%6]  :  (r\^{}n  \mleq{}  (i  \mdiv{}  b))  \mwedge{}  i  \mdiv{}  b  <  (r  +  1)\^{}n
7.  r2  :  \mBbbZ{}
8.  r2  =  (2  *  r)
9.  r2'  :  \mBbbZ{}
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  \mdiv{}  2\^{}n)  *  2\^{}n)  +  (i  rem  2\^{}n))
14.  0  \mleq{}  (i  rem  2\^{}n)
15.  i  rem  2\^{}n  <  2\^{}n
16.  \mneg{}r2'\^{}n  <  i  +  1
\mvdash{}  \mexists{}r:\mBbbN{}  [((r\^{}n  \mleq{}  i)  \mwedge{}  i  <  (r  +  1)\^{}n)]


By

---

Latex:
(With  \mkleeneopen{}r2\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto'  THEN  ElimVar  `r2\mbackslash{}''  THEN  ElimVar  `r2'  THEN  Auto')\mcdot{}

---

Home Index