Metamath Proof Explorer

Theorem bitsshft

Description: Shifting a bit sequence to the left (toward the more significant bits) causes the number to be multiplied by a power of two. (Contributed by Mario Carneiro, 22-Sep-2016)

Ref Expression
Assertion bitsshft 
|- ( ( A e. ZZ /\ N e. NN0 ) -> { n e. NN0 | ( n - N ) e. ( bits ` A ) } = ( bits ` ( A x. ( 2 ^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> A e. ZZ )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> 2 e. NN )
4 simplr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> N e. NN0 )
5 3 4 nnexpcld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( 2 ^ N ) e. NN )
6 5 nnzd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( 2 ^ N ) e. ZZ )
7 dvdsmul2 
 |-  ( ( A e. ZZ /\ ( 2 ^ N ) e. ZZ ) -> ( 2 ^ N ) || ( A x. ( 2 ^ N ) ) )
8 1 6 7 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( 2 ^ N ) || ( A x. ( 2 ^ N ) ) )
9 1 6 zmulcld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( A x. ( 2 ^ N ) ) e. ZZ )
10 bitsuz 
 |-  ( ( ( A x. ( 2 ^ N ) ) e. ZZ /\ N e. NN0 ) -> ( ( 2 ^ N ) || ( A x. ( 2 ^ N ) ) <-> ( bits ` ( A x. ( 2 ^ N ) ) ) C_ ( ZZ>= ` N ) ) )
11 9 4 10 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( 2 ^ N ) || ( A x. ( 2 ^ N ) ) <-> ( bits ` ( A x. ( 2 ^ N ) ) ) C_ ( ZZ>= ` N ) ) )
12 8 11 mpbid 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( bits ` ( A x. ( 2 ^ N ) ) ) C_ ( ZZ>= ` N ) )
13 12 sseld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) -> n e. ( ZZ>= ` N ) ) )
14 uznn0sub 
 |-  ( n e. ( ZZ>= ` N ) -> ( n - N ) e. NN0 )
15 13 14 syl6 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) -> ( n - N ) e. NN0 ) )
16 bitsss 
 |-  ( bits ` A ) C_ NN0
17 16 a1i 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( bits ` A ) C_ NN0 )
18 17 sseld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( n - N ) e. ( bits ` A ) -> ( n - N ) e. NN0 ) )
19 2cnd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> 2 e. CC )
20 2 a1i 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> 2 e. NN )
21 20 nnne0d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> 2 =/= 0 )
22 simplr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> N e. NN0 )
23 22 nn0zd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> N e. ZZ )
24 simprl 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> n e. NN0 )
25 24 nn0zd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> n e. ZZ )
26 19 21 23 25 expsubd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ ( n - N ) ) = ( ( 2 ^ n ) / ( 2 ^ N ) ) )
27 26 oveq2d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( A / ( 2 ^ ( n - N ) ) ) = ( A / ( ( 2 ^ n ) / ( 2 ^ N ) ) ) )
28 simpl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. ZZ )
29 28 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. CC )
30 29 adantr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> A e. CC )
31 20 24 nnexpcld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ n ) e. NN )
32 31 nncnd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ n ) e. CC )
33 20 22 nnexpcld 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ N ) e. NN )
34 33 nncnd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ N ) e. CC )
35 31 nnne0d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ n ) =/= 0 )
36 33 nnne0d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 ^ N ) =/= 0 )
37 30 32 34 35 36 divdiv2d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( A / ( ( 2 ^ n ) / ( 2 ^ N ) ) ) = ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) )
38 27 37 eqtr2d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) = ( A / ( 2 ^ ( n - N ) ) ) )
39 38 fveq2d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( |_ ` ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) ) = ( |_ ` ( A / ( 2 ^ ( n - N ) ) ) ) )
40 39 breq2d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( 2 || ( |_ ` ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) ) <-> 2 || ( |_ ` ( A / ( 2 ^ ( n - N ) ) ) ) ) )
41 40 notbid 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( -. 2 || ( |_ ` ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) ) <-> -. 2 || ( |_ ` ( A / ( 2 ^ ( n - N ) ) ) ) ) )
42 9 adantrr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( A x. ( 2 ^ N ) ) e. ZZ )
43 bitsval2 
 |-  ( ( ( A x. ( 2 ^ N ) ) e. ZZ /\ n e. NN0 ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) <-> -. 2 || ( |_ ` ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) ) ) )
44 42 24 43 syl2anc 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) <-> -. 2 || ( |_ ` ( ( A x. ( 2 ^ N ) ) / ( 2 ^ n ) ) ) ) )
45 bitsval2 
 |-  ( ( A e. ZZ /\ ( n - N ) e. NN0 ) -> ( ( n - N ) e. ( bits ` A ) <-> -. 2 || ( |_ ` ( A / ( 2 ^ ( n - N ) ) ) ) ) )
46 45 ad2ant2rl 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( ( n - N ) e. ( bits ` A ) <-> -. 2 || ( |_ ` ( A / ( 2 ^ ( n - N ) ) ) ) ) )
47 41 44 46 3bitr4d 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ ( n e. NN0 /\ ( n - N ) e. NN0 ) ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) <-> ( n - N ) e. ( bits ` A ) ) )
48 47 expr 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( ( n - N ) e. NN0 -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) <-> ( n - N ) e. ( bits ` A ) ) ) )
49 15 18 48 pm5.21ndd 
 |-  ( ( ( A e. ZZ /\ N e. NN0 ) /\ n e. NN0 ) -> ( n e. ( bits ` ( A x. ( 2 ^ N ) ) ) <-> ( n - N ) e. ( bits ` A ) ) )
50 49 rabbi2dva 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( NN0 i^i ( bits ` ( A x. ( 2 ^ N ) ) ) ) = { n e. NN0 | ( n - N ) e. ( bits ` A ) } )
51 bitsss 
 |-  ( bits ` ( A x. ( 2 ^ N ) ) ) C_ NN0
52 sseqin2 
 |-  ( ( bits ` ( A x. ( 2 ^ N ) ) ) C_ NN0 <-> ( NN0 i^i ( bits ` ( A x. ( 2 ^ N ) ) ) ) = ( bits ` ( A x. ( 2 ^ N ) ) ) )
53 51 52 mpbi 
 |-  ( NN0 i^i ( bits ` ( A x. ( 2 ^ N ) ) ) ) = ( bits ` ( A x. ( 2 ^ N ) ) )
54 50 53 eqtr3di 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> { n e. NN0 | ( n - N ) e. ( bits ` A ) } = ( bits ` ( A x. ( 2 ^ N ) ) ) )