Metamath Proof Explorer

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 ` N ) C_ NN0

Proof

Step Hyp Ref Expression
1 bitsval 
 |-  ( m e. ( bits ` N ) <-> ( N e. ZZ /\ m e. NN0 /\ -. 2 || ( |_ ` ( N / ( 2 ^ m ) ) ) ) )
2 1 simp2bi 
 |-  ( m e. ( bits ` N ) -> m e. NN0 )
3 2 ssriv 
 |-  ( bits ` N ) C_ NN0