Metamath Proof Explorer

Theorem bitsmod

Description: Truncating the bit sequence after some M is equivalent to reducing the argument mod 2 ^ M . (Contributed by Mario Carneiro, 6-Sep-2016)

Ref Expression
Assertion bitsmod 
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( bits ` ( N mod ( 2 ^ M ) ) ) = ( ( bits ` N ) i^i ( 0 ..^ M ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. ZZ )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. NN )
4 simpr 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> M e. NN0 )
5 3 4 nnexpcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. NN )
6 1 5 zmodcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) e. NN0 )
7 6 nn0zd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N mod ( 2 ^ M ) ) e. ZZ )
8 7 biantrurd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) <-> ( ( N mod ( 2 ^ M ) ) e. ZZ /\ ( x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) ) ) )
9 1 ad2antrr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> N e. ZZ )
10 simplr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> x e. NN0 )
11 bitsval2 
 |-  ( ( N e. ZZ /\ x e. NN0 ) -> ( x e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ x ) ) ) ) )
12 9 10 11 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ x ) ) ) ) )
13 simpr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> x < M )
14 13 biantrud 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x e. ( bits ` N ) <-> ( x e. ( bits ` N ) /\ x < M ) ) )
15 2z 
 |-  2 e. ZZ
16 15 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 e. ZZ )
17 9 zred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> N e. RR )
18 2 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 e. NN )
19 18 10 nnexpcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) e. NN )
20 17 19 nndivred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N / ( 2 ^ x ) ) e. RR )
21 20 flcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( N / ( 2 ^ x ) ) ) e. ZZ )
22 7 ad2antrr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N mod ( 2 ^ M ) ) e. ZZ )
23 22 zred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N mod ( 2 ^ M ) ) e. RR )
24 23 19 nndivred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) e. RR )
25 24 flcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) e. ZZ )
26 19 nnzd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) e. ZZ )
27 26 16 zmulcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) x. 2 ) e. ZZ )
28 5 ad2antrr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ M ) e. NN )
29 28 nnzd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ M ) e. ZZ )
30 9 22 zsubcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N - ( N mod ( 2 ^ M ) ) ) e. ZZ )
31 2cnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 e. CC )
32 31 10 expp1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ ( x + 1 ) ) = ( ( 2 ^ x ) x. 2 ) )
33 1nn0 
 |-  1 e. NN0
34 33 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 1 e. NN0 )
35 10 34 nn0addcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x + 1 ) e. NN0 )
36 35 nn0zd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x + 1 ) e. ZZ )
37 simplr 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> M e. NN0 )
38 37 adantr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> M e. NN0 )
39 38 nn0zd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> M e. ZZ )
40 nn0ltp1le 
 |-  ( ( x e. NN0 /\ M e. NN0 ) -> ( x < M <-> ( x + 1 ) <_ M ) )
41 10 38 40 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x < M <-> ( x + 1 ) <_ M ) )
42 13 41 mpbid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( x + 1 ) <_ M )
43 eluz2 
 |-  ( M e. ( ZZ>= ` ( x + 1 ) ) <-> ( ( x + 1 ) e. ZZ /\ M e. ZZ /\ ( x + 1 ) <_ M ) )
44 36 39 42 43 syl3anbrc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> M e. ( ZZ>= ` ( x + 1 ) ) )
45 dvdsexp 
 |-  ( ( 2 e. ZZ /\ ( x + 1 ) e. NN0 /\ M e. ( ZZ>= ` ( x + 1 ) ) ) -> ( 2 ^ ( x + 1 ) ) || ( 2 ^ M ) )
46 16 35 44 45 syl3anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ ( x + 1 ) ) || ( 2 ^ M ) )
47 32 46 eqbrtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) x. 2 ) || ( 2 ^ M ) )
48 28 nnrpd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ M ) e. RR+ )
49 moddifz 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ )
50 17 48 49 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ )
51 2ne0 
 |-  2 =/= 0
52 51 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 =/= 0 )
53 31 52 39 expne0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ M ) =/= 0 )
54 dvdsval2 
 |-  ( ( ( 2 ^ M ) e. ZZ /\ ( 2 ^ M ) =/= 0 /\ ( N - ( N mod ( 2 ^ M ) ) ) e. ZZ ) -> ( ( 2 ^ M ) || ( N - ( N mod ( 2 ^ M ) ) ) <-> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ ) )
55 29 53 30 54 syl3anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ M ) || ( N - ( N mod ( 2 ^ M ) ) ) <-> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ M ) ) e. ZZ ) )
56 50 55 mpbird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ M ) || ( N - ( N mod ( 2 ^ M ) ) ) )
57 27 29 30 47 56 dvdstrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) x. 2 ) || ( N - ( N mod ( 2 ^ M ) ) ) )
58 30 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N - ( N mod ( 2 ^ M ) ) ) e. CC )
59 19 nncnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) e. CC )
60 10 nn0zd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> x e. ZZ )
61 31 52 60 expne0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) =/= 0 )
62 58 59 61 divcan2d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) x. ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) = ( N - ( N mod ( 2 ^ M ) ) ) )
63 57 62 breqtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) x. 2 ) || ( ( 2 ^ x ) x. ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
64 10 nn0red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> x e. RR )
65 38 nn0red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> M e. RR )
66 64 65 13 ltled 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> x <_ M )
67 eluz2 
 |-  ( M e. ( ZZ>= ` x ) <-> ( x e. ZZ /\ M e. ZZ /\ x <_ M ) )
68 60 39 66 67 syl3anbrc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> M e. ( ZZ>= ` x ) )
69 dvdsexp 
 |-  ( ( 2 e. ZZ /\ x e. NN0 /\ M e. ( ZZ>= ` x ) ) -> ( 2 ^ x ) || ( 2 ^ M ) )
70 16 10 68 69 syl3anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) || ( 2 ^ M ) )
71 26 29 30 70 56 dvdstrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 ^ x ) || ( N - ( N mod ( 2 ^ M ) ) ) )
72 dvdsval2 
 |-  ( ( ( 2 ^ x ) e. ZZ /\ ( 2 ^ x ) =/= 0 /\ ( N - ( N mod ( 2 ^ M ) ) ) e. ZZ ) -> ( ( 2 ^ x ) || ( N - ( N mod ( 2 ^ M ) ) ) <-> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. ZZ ) )
73 26 61 30 72 syl3anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( 2 ^ x ) || ( N - ( N mod ( 2 ^ M ) ) ) <-> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. ZZ ) )
74 71 73 mpbid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. ZZ )
75 dvdscmulr 
 |-  ( ( 2 e. ZZ /\ ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. ZZ /\ ( ( 2 ^ x ) e. ZZ /\ ( 2 ^ x ) =/= 0 ) ) -> ( ( ( 2 ^ x ) x. 2 ) || ( ( 2 ^ x ) x. ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) <-> 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
76 16 74 26 61 75 syl112anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( ( 2 ^ x ) x. 2 ) || ( ( 2 ^ x ) x. ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) <-> 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
77 63 76 mpbid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 || ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) )
78 25 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) e. CC )
79 74 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. CC )
80 22 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N mod ( 2 ^ M ) ) e. CC )
81 9 zcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> N e. CC )
82 80 81 pncan3d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( N mod ( 2 ^ M ) ) + ( N - ( N mod ( 2 ^ M ) ) ) ) = N )
83 82 oveq1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( ( N mod ( 2 ^ M ) ) + ( N - ( N mod ( 2 ^ M ) ) ) ) / ( 2 ^ x ) ) = ( N / ( 2 ^ x ) ) )
84 80 58 59 61 divdird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( ( N mod ( 2 ^ M ) ) + ( N - ( N mod ( 2 ^ M ) ) ) ) / ( 2 ^ x ) ) = ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
85 83 84 eqtr3d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( N / ( 2 ^ x ) ) = ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
86 85 fveq2d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( N / ( 2 ^ x ) ) ) = ( |_ ` ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) ) )
87 fladdz 
 |-  ( ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) e. RR /\ ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) e. ZZ ) -> ( |_ ` ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) ) = ( ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
88 24 74 87 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) ) = ( ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
89 86 88 eqtrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( |_ ` ( N / ( 2 ^ x ) ) ) = ( ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) + ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) ) )
90 78 79 89 mvrladdd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( |_ ` ( N / ( 2 ^ x ) ) ) - ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) = ( ( N - ( N mod ( 2 ^ M ) ) ) / ( 2 ^ x ) ) )
91 77 90 breqtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> 2 || ( ( |_ ` ( N / ( 2 ^ x ) ) ) - ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
92 dvdssub2 
 |-  ( ( ( 2 e. ZZ /\ ( |_ ` ( N / ( 2 ^ x ) ) ) e. ZZ /\ ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) e. ZZ ) /\ 2 || ( ( |_ ` ( N / ( 2 ^ x ) ) ) - ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) ) -> ( 2 || ( |_ ` ( N / ( 2 ^ x ) ) ) <-> 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
93 16 21 25 91 92 syl31anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( 2 || ( |_ ` ( N / ( 2 ^ x ) ) ) <-> 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
94 93 notbid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( -. 2 || ( |_ ` ( N / ( 2 ^ x ) ) ) <-> -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
95 12 14 94 3bitr3d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ x < M ) -> ( ( x e. ( bits ` N ) /\ x < M ) <-> -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
96 z0even 
 |-  2 || 0
97 1 ad2antrr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> N e. ZZ )
98 97 zred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> N e. RR )
99 2rp 
 |-  2 e. RR+
100 99 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 2 e. RR+ )
101 37 nn0zd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> M e. ZZ )
102 101 adantr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> M e. ZZ )
103 100 102 rpexpcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ M ) e. RR+ )
104 98 103 modcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( N mod ( 2 ^ M ) ) e. RR )
105 simplr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> x e. NN0 )
106 105 nn0zd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> x e. ZZ )
107 100 106 rpexpcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ x ) e. RR+ )
108 6 ad2antrr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( N mod ( 2 ^ M ) ) e. NN0 )
109 108 nn0ge0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 0 <_ ( N mod ( 2 ^ M ) ) )
110 104 107 109 divge0d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 0 <_ ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) )
111 103 rpred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ M ) e. RR )
112 107 rpred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ x ) e. RR )
113 modlt 
 |-  ( ( N e. RR /\ ( 2 ^ M ) e. RR+ ) -> ( N mod ( 2 ^ M ) ) < ( 2 ^ M ) )
114 98 103 113 syl2anc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( N mod ( 2 ^ M ) ) < ( 2 ^ M ) )
115 100 rpred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 2 e. RR )
116 1le2 
 |-  1 <_ 2
117 116 a1i 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 1 <_ 2 )
118 102 zred 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> M e. RR )
119 105 nn0red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> x e. RR )
120 simpr 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> -. x < M )
121 118 119 120 nltled 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> M <_ x )
122 eluz2 
 |-  ( x e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ x e. ZZ /\ M <_ x ) )
123 102 106 121 122 syl3anbrc 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> x e. ( ZZ>= ` M ) )
124 115 117 123 leexp2ad 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ M ) <_ ( 2 ^ x ) )
125 104 111 112 114 124 ltletrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( N mod ( 2 ^ M ) ) < ( 2 ^ x ) )
126 107 rpcnd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 ^ x ) e. CC )
127 126 mulid1d 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( 2 ^ x ) x. 1 ) = ( 2 ^ x ) )
128 125 127 breqtrrd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( N mod ( 2 ^ M ) ) < ( ( 2 ^ x ) x. 1 ) )
129 1red 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 1 e. RR )
130 104 129 107 ltdivmuld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) < 1 <-> ( N mod ( 2 ^ M ) ) < ( ( 2 ^ x ) x. 1 ) ) )
131 128 130 mpbird 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) < 1 )
132 1e0p1 
 |-  1 = ( 0 + 1 )
133 131 132 breqtrdi 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) < ( 0 + 1 ) )
134 104 107 rerpdivcld 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) e. RR )
135 0z 
 |-  0 e. ZZ
136 flbi 
 |-  ( ( ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) = 0 <-> ( 0 <_ ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) /\ ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) < ( 0 + 1 ) ) ) )
137 134 135 136 sylancl 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) = 0 <-> ( 0 <_ ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) /\ ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) < ( 0 + 1 ) ) ) )
138 110 133 137 mpbir2and 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) = 0 )
139 96 138 breqtrrid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) )
140 120 intnand 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> -. ( x e. ( bits ` N ) /\ x < M ) )
141 139 140 2thd 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) <-> -. ( x e. ( bits ` N ) /\ x < M ) ) )
142 141 con2bid 
 |-  ( ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) /\ -. x < M ) -> ( ( x e. ( bits ` N ) /\ x < M ) <-> -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
143 95 142 pm2.61dan 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> ( ( x e. ( bits ` N ) /\ x < M ) <-> -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
144 101 biantrurd 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> ( ( x e. ( bits ` N ) /\ x < M ) <-> ( M e. ZZ /\ ( x e. ( bits ` N ) /\ x < M ) ) ) )
145 143 144 bitr3d 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> ( -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) <-> ( M e. ZZ /\ ( x e. ( bits ` N ) /\ x < M ) ) ) )
146 an12 
 |-  ( ( M e. ZZ /\ ( x e. ( bits ` N ) /\ x < M ) ) <-> ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) )
147 145 146 bitrdi 
 |-  ( ( ( N e. ZZ /\ M e. NN0 ) /\ x e. NN0 ) -> ( -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) <-> ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) ) )
148 147 pm5.32da 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) <-> ( x e. NN0 /\ ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) ) ) )
149 8 148 bitr3d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ M ) ) e. ZZ /\ ( x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) ) <-> ( x e. NN0 /\ ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) ) ) )
150 3anass 
 |-  ( ( ( N mod ( 2 ^ M ) ) e. ZZ /\ x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) <-> ( ( N mod ( 2 ^ M ) ) e. ZZ /\ ( x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) ) )
151 elfzo2 
 |-  ( x e. ( 0 ..^ M ) <-> ( x e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ x < M ) )
152 elnn0uz 
 |-  ( x e. NN0 <-> x e. ( ZZ>= ` 0 ) )
153 152 3anbi1i 
 |-  ( ( x e. NN0 /\ M e. ZZ /\ x < M ) <-> ( x e. ( ZZ>= ` 0 ) /\ M e. ZZ /\ x < M ) )
154 3anass 
 |-  ( ( x e. NN0 /\ M e. ZZ /\ x < M ) <-> ( x e. NN0 /\ ( M e. ZZ /\ x < M ) ) )
155 151 153 154 3bitr2i 
 |-  ( x e. ( 0 ..^ M ) <-> ( x e. NN0 /\ ( M e. ZZ /\ x < M ) ) )
156 155 anbi2i 
 |-  ( ( x e. ( bits ` N ) /\ x e. ( 0 ..^ M ) ) <-> ( x e. ( bits ` N ) /\ ( x e. NN0 /\ ( M e. ZZ /\ x < M ) ) ) )
157 an12 
 |-  ( ( x e. ( bits ` N ) /\ ( x e. NN0 /\ ( M e. ZZ /\ x < M ) ) ) <-> ( x e. NN0 /\ ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) ) )
158 156 157 bitri 
 |-  ( ( x e. ( bits ` N ) /\ x e. ( 0 ..^ M ) ) <-> ( x e. NN0 /\ ( x e. ( bits ` N ) /\ ( M e. ZZ /\ x < M ) ) ) )
159 149 150 158 3bitr4g 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( ( N mod ( 2 ^ M ) ) e. ZZ /\ x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) <-> ( x e. ( bits ` N ) /\ x e. ( 0 ..^ M ) ) ) )
160 bitsval 
 |-  ( x e. ( bits ` ( N mod ( 2 ^ M ) ) ) <-> ( ( N mod ( 2 ^ M ) ) e. ZZ /\ x e. NN0 /\ -. 2 || ( |_ ` ( ( N mod ( 2 ^ M ) ) / ( 2 ^ x ) ) ) ) )
161 elin 
 |-  ( x e. ( ( bits ` N ) i^i ( 0 ..^ M ) ) <-> ( x e. ( bits ` N ) /\ x e. ( 0 ..^ M ) ) )
162 159 160 161 3bitr4g 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( x e. ( bits ` ( N mod ( 2 ^ M ) ) ) <-> x e. ( ( bits ` N ) i^i ( 0 ..^ M ) ) ) )
163 162 eqrdv 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( bits ` ( N mod ( 2 ^ M ) ) ) = ( ( bits ` N ) i^i ( 0 ..^ M ) ) )