Metamath Proof Explorer

Theorem nnpw2blenfzo

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

Ref Expression
Assertion nnpw2blenfzo 
|- ( N e. NN -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )

Proof

Step Hyp Ref Expression
1 nnpw2blen 
 |-  ( N e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 2z 
 |-  2 e. ZZ
4 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
5 nnm1nn0 
 |-  ( ( #b ` N ) e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
6 4 5 syl 
 |-  ( N e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
7 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( ( #b ` N ) - 1 ) e. NN0 ) -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. ZZ )
8 3 6 7 sylancr 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. ZZ )
9 4 nnnn0d 
 |-  ( N e. NN -> ( #b ` N ) e. NN0 )
10 zexpcl 
 |-  ( ( 2 e. ZZ /\ ( #b ` N ) e. NN0 ) -> ( 2 ^ ( #b ` N ) ) e. ZZ )
11 3 9 10 sylancr 
 |-  ( N e. NN -> ( 2 ^ ( #b ` N ) ) e. ZZ )
12 elfzo 
 |-  ( ( N e. ZZ /\ ( 2 ^ ( ( #b ` N ) - 1 ) ) e. ZZ /\ ( 2 ^ ( #b ` N ) ) e. ZZ ) -> ( N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) <-> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) ) )
13 2 8 11 12 syl3anc 
 |-  ( N e. NN -> ( N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) <-> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) ) )
14 1 13 mpbird 
 |-  ( N e. NN -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )