Metamath Proof Explorer

Theorem bits0

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bits0 
|- ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> -. 2 || N ) )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 bitsval2 
 |-  ( ( N e. ZZ /\ 0 e. NN0 ) -> ( 0 e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ 0 ) ) ) ) )
3 1 2 mpan2 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ 0 ) ) ) ) )
4 2cn 
 |-  2 e. CC
5 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
6 4 5 ax-mp 
 |-  ( 2 ^ 0 ) = 1
7 6 oveq2i 
 |-  ( N / ( 2 ^ 0 ) ) = ( N / 1 )
8 zcn 
 |-  ( N e. ZZ -> N e. CC )
9 8 div1d 
 |-  ( N e. ZZ -> ( N / 1 ) = N )
10 7 9 eqtrid 
 |-  ( N e. ZZ -> ( N / ( 2 ^ 0 ) ) = N )
11 10 fveq2d 
 |-  ( N e. ZZ -> ( |_ ` ( N / ( 2 ^ 0 ) ) ) = ( |_ ` N ) )
12 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
13 11 12 eqtrd 
 |-  ( N e. ZZ -> ( |_ ` ( N / ( 2 ^ 0 ) ) ) = N )
14 13 breq2d 
 |-  ( N e. ZZ -> ( 2 || ( |_ ` ( N / ( 2 ^ 0 ) ) ) <-> 2 || N ) )
15 14 notbid 
 |-  ( N e. ZZ -> ( -. 2 || ( |_ ` ( N / ( 2 ^ 0 ) ) ) <-> -. 2 || N ) )
16 3 15 bitrd 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> -. 2 || N ) )