Metamath Proof Explorer

Theorem bits0ALTV

Description: Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 19-Jun-2020)

Ref Expression
Assertion bits0ALTV ⊢ N ∈ ℤ → 0 ∈ bits ⁡ N ↔ N ∈ Odd

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 bitsval2 ⊢ N ∈ ℤ ∧ 0 ∈ ℕ 0 → 0 ∈ bits ⁡ N ↔ ¬ 2 ∥ N 2 0
3 1 2 mpan2 ⊢ N ∈ ℤ → 0 ∈ bits ⁡ N ↔ ¬ 2 ∥ N 2 0
4 2cn ⊢ 2 ∈ ℂ
5 exp0 ⊢ 2 ∈ ℂ → 2 0 = 1
6 4 5 ax-mp ⊢ 2 0 = 1
7 6 oveq2i ⊢ N 2 0 = N 1
8 zcn ⊢ N ∈ ℤ → N ∈ ℂ
9 8 div1d ⊢ N ∈ ℤ → N 1 = N
10 7 9 syl5eq ⊢ N ∈ ℤ → N 2 0 = N
11 10 fveq2d ⊢ N ∈ ℤ → N 2 0 = N
12 flid ⊢ N ∈ ℤ → N = N
13 11 12 eqtrd ⊢ N ∈ ℤ → N 2 0 = N
14 13 breq2d ⊢ N ∈ ℤ → 2 ∥ N 2 0 ↔ 2 ∥ N
15 14 notbid ⊢ N ∈ ℤ → ¬ 2 ∥ N 2 0 ↔ ¬ 2 ∥ N
16 isodd3 ⊢ N ∈ Odd ↔ N ∈ ℤ ∧ ¬ 2 ∥ N
17 16 baibr ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ N ∈ Odd
18 3 15 17 3bitrd ⊢ N ∈ ℤ → 0 ∈ bits ⁡ N ↔ N ∈ Odd