Metamath Proof Explorer

Theorem blennn

Description: The binary length of a positive integer. (Contributed by AV, 21-May-2020)

Ref Expression
Assertion blennn 
|- ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 nnne0 
 |-  ( N e. NN -> N =/= 0 )
2 blenn0 
 |-  ( ( N e. NN /\ N =/= 0 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
3 1 2 mpdan 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
4 nnre 
 |-  ( N e. NN -> N e. RR )
5 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
6 5 nn0ge0d 
 |-  ( N e. NN -> 0 <_ N )
7 4 6 absidd 
 |-  ( N e. NN -> ( abs ` N ) = N )
8 7 oveq2d 
 |-  ( N e. NN -> ( 2 logb ( abs ` N ) ) = ( 2 logb N ) )
9 8 fveq2d 
 |-  ( N e. NN -> ( |_ ` ( 2 logb ( abs ` N ) ) ) = ( |_ ` ( 2 logb N ) ) )
10 9 oveq1d 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
11 3 10 eqtrd 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )