Metamath Proof Explorer


Theorem nnpw2blen

Description: A positive integer is between 2 to the power of its binary length minus 1 and 2 to the power of its binary length. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion nnpw2blen N 2 # b N 1 N N < 2 # b N

Proof

Step Hyp Ref Expression
1 2rp 2 +
2 1 a1i N 2 +
3 nnrp N N +
4 1ne2 1 2
5 4 necomi 2 1
6 5 a1i N 2 1
7 relogbcl 2 + N + 2 1 log 2 N
8 2 3 6 7 syl3anc N log 2 N
9 8 flcld N log 2 N
10 9 zcnd N log 2 N
11 pncan1 log 2 N log 2 N + 1 - 1 = log 2 N
12 10 11 syl N log 2 N + 1 - 1 = log 2 N
13 12 oveq2d N 2 log 2 N + 1 - 1 = 2 log 2 N
14 blennn N # b N = log 2 N + 1
15 14 oveq1d N # b N 1 = log 2 N + 1 - 1
16 15 oveq2d N 2 # b N 1 = 2 log 2 N + 1 - 1
17 2cnd N 2
18 2ne0 2 0
19 18 a1i N 2 0
20 17 19 9 cxpexpzd N 2 log 2 N = 2 log 2 N
21 13 16 20 3eqtr4d N 2 # b N 1 = 2 log 2 N
22 flle log 2 N log 2 N log 2 N
23 8 22 syl N log 2 N log 2 N
24 2re 2
25 24 a1i N 2
26 1lt2 1 < 2
27 26 a1i N 1 < 2
28 9 zred N log 2 N
29 25 27 28 8 cxpled N log 2 N log 2 N 2 log 2 N 2 log 2 N
30 23 29 mpbid N 2 log 2 N 2 log 2 N
31 2cn 2
32 eldifpr 2 0 1 2 2 0 2 1
33 31 18 5 32 mpbir3an 2 0 1
34 nncn N N
35 nnne0 N N 0
36 eldifsn N 0 N N 0
37 34 35 36 sylanbrc N N 0
38 cxplogb 2 0 1 N 0 2 log 2 N = N
39 33 37 38 sylancr N 2 log 2 N = N
40 30 39 breqtrd N 2 log 2 N N
41 21 40 eqbrtrd N 2 # b N 1 N
42 flltp1 log 2 N log 2 N < log 2 N + 1
43 8 42 syl N log 2 N < log 2 N + 1
44 9 peano2zd N log 2 N + 1
45 44 zred N log 2 N + 1
46 25 27 8 45 cxpltd N log 2 N < log 2 N + 1 2 log 2 N < 2 log 2 N + 1
47 43 46 mpbid N 2 log 2 N < 2 log 2 N + 1
48 17 19 44 cxpexpzd N 2 log 2 N + 1 = 2 log 2 N + 1
49 47 39 48 3brtr3d N N < 2 log 2 N + 1
50 14 oveq2d N 2 # b N = 2 log 2 N + 1
51 49 50 breqtrrd N N < 2 # b N
52 41 51 jca N 2 # b N 1 N N < 2 # b N