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	⊢ ( bits ‘ 𝑁 ) ⊆ ℕ0

Proof

Step	Hyp	Ref	Expression
1		bitsval	⊢ ( 𝑚 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
2	1	simp2bi	⊢ ( 𝑚 ∈ ( bits ‘ 𝑁 ) → 𝑚 ∈ ℕ0 )
3	2	ssriv	⊢ ( bits ‘ 𝑁 ) ⊆ ℕ0