---

Step * 2 1 1 1 of Lemma integer-nth-root


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
18. ((2 * r) + 1)^n ≤ i
⊢ ((i ÷ 2^n) * 2^n) + (i rem 2^n) < (2 * (r + 1))^n
BY
{ (Assert ⌜(2^n * ((i ÷ 2^n) + 1)) ≤ (2^n * (r + 1)^n)⌝⋅ THEN Auto') }

1
.....assertion..... 
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
18. ((2 * r) + 1)^n ≤ i
⊢ (2^n * ((i ÷ 2^n) + 1)) ≤ (2^n * (r + 1)^n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  b  :  \{b:\mBbbZ{}|  1  <  b\} 
3.  b  =  2\^{}n
4.  i  :  \mBbbN{}\msupplus{}
5.  r  :  \mBbbN{}
6.  r\^{}n  \mleq{}  (i  \mdiv{}  b)
7.  i  \mdiv{}  b  <  (r  +  1)\^{}n
8.  r2  :  \mBbbZ{}
9.  2  *  r  \mmember{}  \mBbbZ{}
10.  r2'  :  \mBbbZ{}
11.  (2  *  r)  +  1  \mmember{}  \mBbbZ{}
12.  (2  *  r)\^{}n  =  (2\^{}n  *  r\^{}n)
13.  (2  *  (r  +  1))\^{}n  =  (2\^{}n  *  (r  +  1)\^{}n)
14.  i  =  (((i  \mdiv{}  2\^{}n)  *  2\^{}n)  +  (i  rem  2\^{}n))
15.  0  \mleq{}  (i  rem  2\^{}n)
16.  i  rem  2\^{}n  <  2\^{}n
17.  ((2  *  r)  +  1)\^{}n  <  i  +  1
18.  ((2  *  r)  +  1)\^{}n  \mleq{}  i
\mvdash{}  ((i  \mdiv{}  2\^{}n)  *  2\^{}n)  +  (i  rem  2\^{}n)  <  (2  *  (r  +  1))\^{}n


By

---

Latex:
(Assert  \mkleeneopen{}(2\^{}n  *  ((i  \mdiv{}  2\^{}n)  +  1))  \mleq{}  (2\^{}n  *  (r  +  1)\^{}n)\mkleeneclose{}\mcdot{}  THEN  Auto')

---

Home Index