Theorem bitsfval

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

	Ref	Expression
Assertion	bitsfval	$$⊢N\in \mathbb{Z}\to \mathrm{bits}\left(N\right)=\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{N}{2^m}⌋\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fvoveq1	$$⊢n=N\to ⌊\frac{n}{2^m}⌋=⌊\frac{N}{2^m}⌋$$
2	1	breq2d	$$⊢n=N\to \left(2\parallel ⌊\frac{n}{2^m}⌋\leftrightarrow 2\parallel ⌊\frac{N}{2^m}⌋\right)$$
3	2	notbid	$$⊢n=N\to \left(\neg 2\parallel ⌊\frac{n}{2^m}⌋\leftrightarrow \neg 2\parallel ⌊\frac{N}{2^m}⌋\right)$$
4	3	rabbidv	$$⊢n=N\to \left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}=\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{N}{2^m}⌋\right\}$$
5		df-bits	$$⊢\mathrm{bits}=\left(n\in \mathbb{Z}⟼\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}\right)$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7	6	rabex	$$⊢\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{N}{2^m}⌋\right\}\in \mathrm{V}$$
8	4 5 7	fvmpt	$$⊢N\in \mathbb{Z}\to \mathrm{bits}\left(N\right)=\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{N}{2^m}⌋\right\}$$