Metamath Proof Explorer

Theorem bits0e

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

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

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 bits0 
 |-  ( ( 2 x. N ) e. ZZ -> ( 0 e. ( bits ` ( 2 x. N ) ) <-> -. 2 || ( 2 x. N ) ) )
8 6 7 syl 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` ( 2 x. N ) ) <-> -. 2 || ( 2 x. N ) ) )
9 8 con2bid 
 |-  ( N e. ZZ -> ( 2 || ( 2 x. N ) <-> -. 0 e. ( bits ` ( 2 x. N ) ) ) )
10 3 9 mpbid 
 |-  ( N e. ZZ -> -. 0 e. ( bits ` ( 2 x. N ) ) )