bitsval2

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

		Ref	Expression
	Assertion	bitsval2	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$

Step	Hyp	Ref	Expression
1		bitsval	$⊢ M \in bits (N) \leftrightarrow (N \in ℤ \land M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
2		df-3an	$⊢ (N \in ℤ \land M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋) \leftrightarrow ((N \in ℤ \land M \in ℕ_{0}) \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
3	1 2	bitri	$⊢ M \in bits (N) \leftrightarrow ((N \in ℤ \land M \in ℕ_{0}) \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
4	3	baib	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (M \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$

Metamath Proof Explorer