Metamath Proof Explorer

Theorem bits0o

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

Ref Expression
Assertion bits0o ⊢ N ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N + 1

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 dvdsmul1 ⊢ 2 ∈ ℤ ∧ N ∈ ℤ → 2 ∥ 2 ⋅ N
3 1 2 mpan ⊢ N ∈ ℤ → 2 ∥ 2 ⋅ N
4 1 a1i ⊢ N ∈ ℤ → 2 ∈ ℤ
5 id ⊢ N ∈ ℤ → N ∈ ℤ
6 4 5 zmulcld ⊢ N ∈ ℤ → 2 ⋅ N ∈ ℤ
7 2nn ⊢ 2 ∈ ℕ
8 7 a1i ⊢ N ∈ ℤ → 2 ∈ ℕ
9 1lt2 ⊢ 1 < 2
10 9 a1i ⊢ N ∈ ℤ → 1 < 2
11 ndvdsp1 ⊢ 2 ⋅ N ∈ ℤ ∧ 2 ∈ ℕ ∧ 1 < 2 → 2 ∥ 2 ⋅ N → ¬ 2 ∥ 2 ⋅ N + 1
12 6 8 10 11 syl3anc ⊢ N ∈ ℤ → 2 ∥ 2 ⋅ N → ¬ 2 ∥ 2 ⋅ N + 1
13 3 12 mpd ⊢ N ∈ ℤ → ¬ 2 ∥ 2 ⋅ N + 1
14 6 peano2zd ⊢ N ∈ ℤ → 2 ⋅ N + 1 ∈ ℤ
15 bits0 ⊢ 2 ⋅ N + 1 ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N + 1 ↔ ¬ 2 ∥ 2 ⋅ N + 1
16 14 15 syl ⊢ N ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N + 1 ↔ ¬ 2 ∥ 2 ⋅ N + 1
17 13 16 mpbird ⊢ N ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N + 1