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

.....assertion..... 
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
18. ((2 r) 1)^n ≤ i
⊢ (2^n ((i ÷ 2^n) 1)) ≤ (2^n (r 1)^n)
BY
xxx(BLemma `mul_preserves_le`  THEN Auto)xxx }


Latex:


Latex:
.....assertion..... 
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{}  (2\^{}n  *  ((i  \mdiv{}  2\^{}n)  +  1))  \mleq{}  (2\^{}n  *  (r  +  1)\^{}n)


By


Latex:
xxx(BLemma  `mul\_preserves\_le`    THEN  Auto)xxx




Home Index