Metamath Proof Explorer

Theorem bitsfi

Description: Every number is associated with a finite set of bits. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsfi 
|- ( N e. NN0 -> ( bits ` N ) e. Fin )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 2re 
 |-  2 e. RR
3 2 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
4 1lt2 
 |-  1 < 2
5 4 a1i 
 |-  ( N e. NN0 -> 1 < 2 )
6 expnbnd 
 |-  ( ( N e. RR /\ 2 e. RR /\ 1 < 2 ) -> E. m e. NN N < ( 2 ^ m ) )
7 1 3 5 6 syl3anc 
 |-  ( N e. NN0 -> E. m e. NN N < ( 2 ^ m ) )
8 fzofi 
 |-  ( 0 ..^ m ) e. Fin
9 simpl 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> N e. NN0 )
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtrdi 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> N e. ( ZZ>= ` 0 ) )
12 2nn 
 |-  2 e. NN
13 12 a1i 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> 2 e. NN )
14 simprl 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> m e. NN )
15 14 nnnn0d 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> m e. NN0 )
16 13 15 nnexpcld 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> ( 2 ^ m ) e. NN )
17 16 nnzd 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> ( 2 ^ m ) e. ZZ )
18 simprr 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> N < ( 2 ^ m ) )
19 elfzo2 
 |-  ( N e. ( 0 ..^ ( 2 ^ m ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( 2 ^ m ) e. ZZ /\ N < ( 2 ^ m ) ) )
20 11 17 18 19 syl3anbrc 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> N e. ( 0 ..^ ( 2 ^ m ) ) )
21 9 nn0zd 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> N e. ZZ )
22 bitsfzo 
 |-  ( ( N e. ZZ /\ m e. NN0 ) -> ( N e. ( 0 ..^ ( 2 ^ m ) ) <-> ( bits ` N ) C_ ( 0 ..^ m ) ) )
23 21 15 22 syl2anc 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> ( N e. ( 0 ..^ ( 2 ^ m ) ) <-> ( bits ` N ) C_ ( 0 ..^ m ) ) )
24 20 23 mpbid 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> ( bits ` N ) C_ ( 0 ..^ m ) )
25 ssfi 
 |-  ( ( ( 0 ..^ m ) e. Fin /\ ( bits ` N ) C_ ( 0 ..^ m ) ) -> ( bits ` N ) e. Fin )
26 8 24 25 sylancr 
 |-  ( ( N e. NN0 /\ ( m e. NN /\ N < ( 2 ^ m ) ) ) -> ( bits ` N ) e. Fin )
27 7 26 rexlimddv 
 |-  ( N e. NN0 -> ( bits ` N ) e. Fin )