Theorem bitsval2

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

	Ref	Expression
Assertion	bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bitsval	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
2		df-3an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
3	1 2	bitri	⊢ ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )
4	3	baib	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑀 ) ) ) ) )