Metamath Proof Explorer

Theorem blenval

Description: The binary length of an integer. (Contributed by AV, 20-May-2020)

Ref Expression
Assertion blenval 
|- ( N e. V -> ( #b ` N ) = if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 df-blen 
 |-  #b = ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )
2 eqeq1 
 |-  ( n = N -> ( n = 0 <-> N = 0 ) )
3 fveq2 
 |-  ( n = N -> ( abs ` n ) = ( abs ` N ) )
4 3 oveq2d 
 |-  ( n = N -> ( 2 logb ( abs ` n ) ) = ( 2 logb ( abs ` N ) ) )
5 4 fveq2d 
 |-  ( n = N -> ( |_ ` ( 2 logb ( abs ` n ) ) ) = ( |_ ` ( 2 logb ( abs ` N ) ) ) )
6 5 oveq1d 
 |-  ( n = N -> ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
7 2 6 ifbieq2d 
 |-  ( n = N -> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) = if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )
8 elex 
 |-  ( N e. V -> N e. _V )
9 1ex 
 |-  1 e. _V
10 ovex 
 |-  ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) e. _V
11 9 10 ifex 
 |-  if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) e. _V
12 11 a1i 
 |-  ( N e. V -> if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) e. _V )
13 1 7 8 12 fvmptd3 
 |-  ( N e. V -> ( #b ` N ) = if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )