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 ∈ Odd → 0 ∈ bits ⁡ N

Proof

Step Hyp Ref Expression
1 oddz ⊢ N ∈ Odd → N ∈ ℤ
2 bits0ALTV ⊢ N ∈ ℤ → 0 ∈ bits ⁡ N ↔ N ∈ Odd
3 1 2 syl ⊢ N ∈ Odd → 0 ∈ bits ⁡ N ↔ N ∈ Odd
4 3 ibir ⊢ N ∈ Odd → 0 ∈ bits ⁡ N