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 e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) )

Proof

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