Metamath Proof Explorer

Theorem nnpw2blenfzo2

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

Ref Expression
Assertion nnpw2blenfzo2 
|- ( N e. NN -> ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nnpw2blenfzo 
 |-  ( N e. NN -> N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) )
2 elfzolborelfzop1 
 |-  ( N e. ( ( 2 ^ ( ( #b ` N ) - 1 ) ) ..^ ( 2 ^ ( #b ` N ) ) ) -> ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) )
3 1 2 syl 
 |-  ( N e. NN -> ( N = ( 2 ^ ( ( #b ` N ) - 1 ) ) \/ N e. ( ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + 1 ) ..^ ( 2 ^ ( #b ` N ) ) ) ) )