bitsval

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

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

Step	Hyp	Ref	Expression
1		df-bits	$⊢ bits = (n \in ℤ ⟼ \{m \in ℕ_{0} \| \neg 2 ∥ ⌊\frac{n}{2^{m}}⌋\})$
2	1	mptrcl	$⊢ M \in bits (N) \to N \in ℤ$
3		bitsfval	$⊢ N \in ℤ \to bits (N) = \{m \in ℕ_{0} \| \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋\}$
4	3	eleq2d	$⊢ N \in ℤ \to (M \in bits (N) \leftrightarrow M \in \{m \in ℕ_{0} \| \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋\})$
5		oveq2	$⊢ m = M \to 2^{m} = 2^{M}$
6	5	oveq2d	$⊢ m = M \to \frac{N}{2^{m}} = \frac{N}{2^{M}}$
7	6	fveq2d	$⊢ m = M \to ⌊\frac{N}{2^{m}}⌋ = ⌊\frac{N}{2^{M}}⌋$
8	7	breq2d	$⊢ m = M \to (2 ∥ ⌊\frac{N}{2^{m}}⌋ \leftrightarrow 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
9	8	notbid	$⊢ m = M \to (\neg 2 ∥ ⌊\frac{N}{2^{m}}⌋ \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
10	9	elrab	$⊢ M \in \{m \in ℕ_{0} \| \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋\} \leftrightarrow (M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$
11	4 10	bitrdi	$⊢ N \in ℤ \to (M \in bits (N) \leftrightarrow (M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋))$
12	2 11	biadanii	$⊢ M \in bits (N) \leftrightarrow (N \in ℤ \land (M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋))$
13		3anass	$⊢ (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}}⌋))$
14	12 13	bitr4i	$⊢ M \in bits (N) \leftrightarrow (N \in ℤ \land M \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N}{2^{M}}⌋)$

Metamath Proof Explorer