Metamath Proof Explorer

Theorem bitsfval

Description: Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsfval 
|- ( N e. ZZ -> ( bits ` N ) = { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } )

Proof

Step Hyp Ref Expression
1 fvoveq1 
 |-  ( n = N -> ( |_ ` ( n / ( 2 ^ m ) ) ) = ( |_ ` ( N / ( 2 ^ m ) ) ) )
2 1 breq2d 
 |-  ( n = N -> ( 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) <-> 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
3 2 notbid 
 |-  ( n = N -> ( -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
4 3 rabbidv 
 |-  ( n = N -> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } = { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } )
5 df-bits 
 |-  bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
6 nn0ex 
 |-  NN0 e. _V
7 6 rabex 
 |-  { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } e. _V
8 4 5 7 fvmpt 
 |-  ( N e. ZZ -> ( bits ` N ) = { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } )