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


1. : ℕ+
2. {b:ℤ1 < b} 
3. 2^n ∈ {b:ℤ1 < b} 
4. : ℕ+
5. : ℕ
6. r^n ≤ (i ÷ b)
7. i ÷ b < (r 1)^n
8. r2 : ℤ
9. 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 ÷ 2^n) 2^n) (i rem 2^n)) ∈ ℤ
15. 0 ≤ (i rem 2^n)
16. rem 2^n < 2^n
17. ¬((2 r) 1)^n < 1
⊢ (2 r)^n ≤ i
BY
Auto' }

1
1. : ℕ+
2. {b:ℤ1 < b} 
3. 2^n ∈ {b:ℤ1 < b} 
4. : ℕ+
5. : ℕ
6. r^n ≤ (i ÷ b)
7. i ÷ b < (r 1)^n
8. r2 : ℤ
9. 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 ÷ 2^n) 2^n) (i rem 2^n)) ∈ ℤ
15. 0 ≤ (i rem 2^n)
16. rem 2^n < 2^n
17. ¬((2 r) 1)^n < 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.  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.  \mneg{}((2  *  r)  +  1)\^{}n  <  i  +  1
\mvdash{}  (2  *  r)\^{}n  \mleq{}  i


By


Latex:
Auto'




Home Index