Theorem bits0o

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

	Ref	Expression
Assertion	bits0o	⊢ ( 𝑁 ∈ ℤ → 0 ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) )

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		2nn	⊢ 2 ∈ ℕ
8	7	a1i	⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℕ )
9		1lt2	⊢ 1 < 2
10	9	a1i	⊢ ( 𝑁 ∈ ℤ → 1 < 2 )
11		ndvdsp1	⊢ ( ( ( 2 · 𝑁 ) ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2 ) → ( 2 ∥ ( 2 · 𝑁 ) → ¬ 2 ∥ ( ( 2 · 𝑁 ) + 1 ) ) )
12	6 8 10 11	syl3anc	⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 2 · 𝑁 ) → ¬ 2 ∥ ( ( 2 · 𝑁 ) + 1 ) ) )
13	3 12	mpd	⊢ ( 𝑁 ∈ ℤ → ¬ 2 ∥ ( ( 2 · 𝑁 ) + 1 ) )
14	6	peano2zd	⊢ ( 𝑁 ∈ ℤ → ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ )
15		bits0	⊢ ( ( ( 2 · 𝑁 ) + 1 ) ∈ ℤ → ( 0 ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ ¬ 2 ∥ ( ( 2 · 𝑁 ) + 1 ) ) )
16	14 15	syl	⊢ ( 𝑁 ∈ ℤ → ( 0 ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) ↔ ¬ 2 ∥ ( ( 2 · 𝑁 ) + 1 ) ) )
17	13 16	mpbird	⊢ ( 𝑁 ∈ ℤ → 0 ∈ ( bits ‘ ( ( 2 · 𝑁 ) + 1 ) ) )