Metamath Proof Explorer

Theorem bits0o

Description: The zeroth bit of an odd number is one. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bits0o 
|- ( N e. ZZ -> 0 e. ( bits ` ( ( 2 x. N ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 dvdsmul1 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> 2 || ( 2 x. N ) )
3 1 2 mpan 
 |-  ( N e. ZZ -> 2 || ( 2 x. N ) )
4 1 a1i 
 |-  ( N e. ZZ -> 2 e. ZZ )
5 id 
 |-  ( N e. ZZ -> N e. ZZ )
6 4 5 zmulcld 
 |-  ( N e. ZZ -> ( 2 x. N ) e. ZZ )
7 2nn 
 |-  2 e. NN
8 7 a1i 
 |-  ( N e. ZZ -> 2 e. NN )
9 1lt2 
 |-  1 < 2
10 9 a1i 
 |-  ( N e. ZZ -> 1 < 2 )
11 ndvdsp1 
 |-  ( ( ( 2 x. N ) e. ZZ /\ 2 e. NN /\ 1 < 2 ) -> ( 2 || ( 2 x. N ) -> -. 2 || ( ( 2 x. N ) + 1 ) ) )
12 6 8 10 11 syl3anc 
 |-  ( N e. ZZ -> ( 2 || ( 2 x. N ) -> -. 2 || ( ( 2 x. N ) + 1 ) ) )
13 3 12 mpd 
 |-  ( N e. ZZ -> -. 2 || ( ( 2 x. N ) + 1 ) )
14 6 peano2zd 
 |-  ( N e. ZZ -> ( ( 2 x. N ) + 1 ) e. ZZ )
15 bits0 
 |-  ( ( ( 2 x. N ) + 1 ) e. ZZ -> ( 0 e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> -. 2 || ( ( 2 x. N ) + 1 ) ) )
16 14 15 syl 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> -. 2 || ( ( 2 x. N ) + 1 ) ) )
17 13 16 mpbird 
 |-  ( N e. ZZ -> 0 e. ( bits ` ( ( 2 x. N ) + 1 ) ) )