Metamath Proof Explorer

Theorem bitsval

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

Ref Expression
Assertion bitsval 
|- ( M e. ( bits ` N ) <-> ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-bits 
 |-  bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
2 1 mptrcl 
 |-  ( M e. ( bits ` N ) -> N e. ZZ )
3 bitsfval 
 |-  ( N e. ZZ -> ( bits ` N ) = { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } )
4 3 eleq2d 
 |-  ( N e. ZZ -> ( M e. ( bits ` N ) <-> M e. { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } ) )
5 oveq2 
 |-  ( m = M -> ( 2 ^ m ) = ( 2 ^ M ) )
6 5 oveq2d 
 |-  ( m = M -> ( N / ( 2 ^ m ) ) = ( N / ( 2 ^ M ) ) )
7 6 fveq2d 
 |-  ( m = M -> ( |_ ` ( N / ( 2 ^ m ) ) ) = ( |_ ` ( N / ( 2 ^ M ) ) ) )
8 7 breq2d 
 |-  ( m = M -> ( 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) <-> 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
9 8 notbid 
 |-  ( m = M -> ( -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
10 9 elrab 
 |-  ( M e. { m e. NN0 | -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) } <-> ( M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )
11 4 10 bitrdi 
 |-  ( N e. ZZ -> ( M e. ( bits ` N ) <-> ( M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) ) )
12 2 11 biadanii 
 |-  ( M e. ( bits ` N ) <-> ( N e. ZZ /\ ( M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) ) )
13 3anass 
 |-  ( ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) <-> ( N e. ZZ /\ ( M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) ) )
14 12 13 bitr4i 
 |-  ( M e. ( bits ` N ) <-> ( N e. ZZ /\ M e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ M ) ) ) ) )