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 ) ) |
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 ) ) |