Metamath Proof Explorer

Theorem bits0e

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

Ref Expression
Assertion bits0e ⊢ N ∈ ℤ → ¬ 0 ∈ bits ⁡ 2 ⋅ N

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 bits0 ⊢ 2 ⋅ N ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N ↔ ¬ 2 ∥ 2 ⋅ N
8 6 7 syl ⊢ N ∈ ℤ → 0 ∈ bits ⁡ 2 ⋅ N ↔ ¬ 2 ∥ 2 ⋅ N
9 8 con2bid ⊢ N ∈ ℤ → 2 ∥ 2 ⋅ N ↔ ¬ 0 ∈ bits ⁡ 2 ⋅ N
10 3 9 mpbid ⊢ N ∈ ℤ → ¬ 0 ∈ bits ⁡ 2 ⋅ N