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	⊢ ( 𝑁 ∈ Even → ¬ 0 ∈ ( bits ‘ 𝑁 ) )

Proof

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