Theorem bitsss

Description: The set of bits of an integer is a subset of NN0 . (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	bitsss	$$⊢\mathrm{bits}\left(N\right)\subseteq {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		bitsval	$$⊢m\in \mathrm{bits}\left(N\right)\leftrightarrow \left(N\in \mathbb{Z}\wedge m\in {\mathbb{N}}_0\wedge \neg 2\parallel ⌊\frac{N}{2^m}⌋\right)$$
2	1	simp2bi	$$⊢m\in \mathrm{bits}\left(N\right)\to m\in {\mathbb{N}}_0$$
3	2	ssriv	$$⊢\mathrm{bits}\left(N\right)\subseteq {\mathbb{N}}_0$$