Metamath Proof Explorer


Theorem bits0eALTV

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

Ref Expression
Assertion bits0eALTV
|- ( N e. Even -> -. 0 e. ( bits ` N ) )

Proof

Step Hyp Ref Expression
1 evennodd
 |-  ( N e. Even -> -. N e. Odd )
2 evenz
 |-  ( N e. Even -> N e. ZZ )
3 bits0ALTV
 |-  ( N e. ZZ -> ( 0 e. ( bits ` N ) <-> N e. Odd ) )
4 2 3 syl
 |-  ( N e. Even -> ( 0 e. ( bits ` N ) <-> N e. Odd ) )
5 1 4 mtbird
 |-  ( N e. Even -> -. 0 e. ( bits ` N ) )