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

Proof

Step	Hyp	Ref	Expression
1		oddz	⊢ ( 𝑁 ∈ Odd → 𝑁 ∈ ℤ )
2		bits0ALTV	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ 𝑁 ∈ Odd ) )
3	1 2	syl	⊢ ( 𝑁 ∈ Odd → ( 0 ∈ ( bits ‘ 𝑁 ) ↔ 𝑁 ∈ Odd ) )
4	3	ibir	⊢ ( 𝑁 ∈ Odd → 0 ∈ ( bits ‘ 𝑁 ) )