Theorem bits0e

Description: The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bits0e	⊢ ( 𝑁 ∈ ℤ → ¬ 0 ∈ ( bits ‘ ( 2 · 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2z	⊢ 2 ∈ ℤ
2		dvdsmul1	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 2 ∥ ( 2 · 𝑁 ) )
3	1 2	mpan	⊢ ( 𝑁 ∈ ℤ → 2 ∥ ( 2 · 𝑁 ) )
4	1	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℤ )
5		id	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℤ )
6	4 5	zmulcld	⊢ ( 𝑁 ∈ ℤ → ( 2 · 𝑁 ) ∈ ℤ )
7		bits0	⊢ ( ( 2 · 𝑁 ) ∈ ℤ → ( 0 ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ ¬ 2 ∥ ( 2 · 𝑁 ) ) )
8	6 7	syl	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ ( 2 · 𝑁 ) ) ↔ ¬ 2 ∥ ( 2 · 𝑁 ) ) )
9	8	con2bid	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 2 · 𝑁 ) ↔ ¬ 0 ∈ ( bits ‘ ( 2 · 𝑁 ) ) ) )
10	3 9	mpbid	⊢ ( 𝑁 ∈ ℤ → ¬ 0 ∈ ( bits ‘ ( 2 · 𝑁 ) ) )