Metamath Proof Explorer

Theorem bits0oALTV

Description: The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion bits0oALTV 
|- ( N e. Odd -> 0 e. ( bits ` N ) )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( N e. Odd -> N e. ZZ )
2 bits0ALTV 
 |-  ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> N e. Odd ) )
3 1 2 syl 
 |-  ( N e. Odd -> ( 0 e. ( bits ` N ) <-> N e. Odd ) )
4 3 ibir 
 |-  ( N e. Odd -> 0 e. ( bits ` N ) )