Metamath Proof Explorer

Theorem bits0ALTV

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

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

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 syl5eq 
 |-  ( 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 isodd3 
 |-  ( N e. Odd <-> ( N e. ZZ /\ -. 2 || N ) )
17 16 baibr 
 |-  ( N e. ZZ -> ( -. 2 || N <-> N e. Odd ) )
18 3 15 17 3bitrd 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> N e. Odd ) )