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

Proof

Step Hyp Ref Expression
1 evennodd ⊢ N ∈ Even → ¬ N ∈ Odd
2 evenz ⊢ N ∈ Even → N ∈ ℤ
3 bits0ALTV ⊢ N ∈ ℤ → 0 ∈ bits ⁡ N ↔ N ∈ Odd
4 2 3 syl ⊢ N ∈ Even → 0 ∈ bits ⁡ N ↔ N ∈ Odd
5 1 4 mtbird ⊢ N ∈ Even → ¬ 0 ∈ bits ⁡ N