Metamath Proof Explorer

Theorem bitsval2

Description: Expand the definition of the bits of an integer. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsval2 ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M ∈ bits ⁡ N ↔ ¬ 2 ∥ N 2 M

Proof

Step Hyp Ref Expression
1 bitsval ⊢ M ∈ bits ⁡ N ↔ N ∈ ℤ ∧ M ∈ ℕ 0 ∧ ¬ 2 ∥ N 2 M
2 df-3an ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 ∧ ¬ 2 ∥ N 2 M ↔ N ∈ ℤ ∧ M ∈ ℕ 0 ∧ ¬ 2 ∥ N 2 M
3 1 2 bitri ⊢ M ∈ bits ⁡ N ↔ N ∈ ℤ ∧ M ∈ ℕ 0 ∧ ¬ 2 ∥ N 2 M
4 3 baib ⊢ N ∈ ℤ ∧ M ∈ ℕ 0 → M ∈ bits ⁡ N ↔ ¬ 2 ∥ N 2 M