Metamath Proof Explorer

Theorem bitsres

Description: Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsres 
|- ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. ZZ )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> 2 e. NN )
4 simpr 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> N e. NN0 )
5 3 4 nnexpcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. NN )
6 1 5 zmodcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. NN0 )
7 6 nn0zd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. ZZ )
8 7 znegcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> -u ( A mod ( 2 ^ N ) ) e. ZZ )
9 sadadd 
 |-  ( ( -u ( A mod ( 2 ^ N ) ) e. ZZ /\ A e. ZZ ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) )
10 8 1 9 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) )
11 sadadd 
 |-  ( ( -u ( A mod ( 2 ^ N ) ) e. ZZ /\ ( A mod ( 2 ^ N ) ) e. ZZ ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) )
12 8 7 11 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) )
13 8 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> -u ( A mod ( 2 ^ N ) ) e. CC )
14 7 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A mod ( 2 ^ N ) ) e. CC )
15 13 14 addcomd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) = ( ( A mod ( 2 ^ N ) ) + -u ( A mod ( 2 ^ N ) ) ) )
16 14 negidd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( A mod ( 2 ^ N ) ) + -u ( A mod ( 2 ^ N ) ) ) = 0 )
17 15 16 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) = 0 )
18 17 fveq2d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) = ( bits ` 0 ) )
19 0bits 
 |-  ( bits ` 0 ) = (/)
20 18 19 eqtrdi 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + ( A mod ( 2 ^ N ) ) ) ) = (/) )
21 12 20 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) = (/) )
22 21 oveq1d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) )
23 bitsss 
 |-  ( bits ` -u ( A mod ( 2 ^ N ) ) ) C_ NN0
24 bitsss 
 |-  ( bits ` ( A mod ( 2 ^ N ) ) ) C_ NN0
25 inss1 
 |-  ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ ( bits ` A )
26 bitsss 
 |-  ( bits ` A ) C_ NN0
27 26 a1i 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` A ) C_ NN0 )
28 25 27 sstrid 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 )
29 sadass 
 |-  ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) C_ NN0 /\ ( bits ` ( A mod ( 2 ^ N ) ) ) C_ NN0 /\ ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) )
30 23 24 28 29 mp3an12i 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) )
31 bitsmod 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( A mod ( 2 ^ N ) ) ) = ( ( bits ` A ) i^i ( 0 ..^ N ) ) )
32 31 oveq1d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) )
33 inss1 
 |-  ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ ( bits ` A )
34 33 27 sstrid 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( 0 ..^ N ) ) C_ NN0 )
35 fzouzdisj 
 |-  ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) = (/)
36 35 ineq2i 
 |-  ( ( bits ` A ) i^i ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i (/) )
37 inindi 
 |-  ( ( bits ` A ) i^i ( ( 0 ..^ N ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) )
38 in0 
 |-  ( ( bits ` A ) i^i (/) ) = (/)
39 36 37 38 3eqtr3i 
 |-  ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = (/)
40 39 a1i 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) i^i ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = (/) )
41 34 28 40 saddisj 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) u. ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) )
42 indi 
 |-  ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) u. ( ( bits ` A ) i^i ( ZZ>= ` N ) ) )
43 41 42 eqtr4di 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) )
44 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
45 4 44 eleqtrdi 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
46 fzouzsplit 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) )
47 45 46 syl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) )
48 44 47 syl5eq 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> NN0 = ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) )
49 26 48 sseqtrid 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` A ) C_ ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) )
50 df-ss 
 |-  ( ( bits ` A ) C_ ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) <-> ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( bits ` A ) )
51 49 50 sylib 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ( 0 ..^ N ) u. ( ZZ>= ` N ) ) ) = ( bits ` A ) )
52 43 51 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` A ) i^i ( 0 ..^ N ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( bits ` A ) )
53 32 52 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( bits ` A ) )
54 53 oveq2d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` ( A mod ( 2 ^ N ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) )
55 30 54 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` ( A mod ( 2 ^ N ) ) ) ) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) )
56 sadid2 
 |-  ( ( ( bits ` A ) i^i ( ZZ>= ` N ) ) C_ NN0 -> ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) )
57 28 56 syl 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( (/) sadd ( ( bits ` A ) i^i ( ZZ>= ` N ) ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) )
58 22 55 57 3eqtr3d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` -u ( A mod ( 2 ^ N ) ) ) sadd ( bits ` A ) ) = ( ( bits ` A ) i^i ( ZZ>= ` N ) ) )
59 1 zcnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. CC )
60 13 59 addcomd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + A ) = ( A + -u ( A mod ( 2 ^ N ) ) ) )
61 59 14 negsubd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A + -u ( A mod ( 2 ^ N ) ) ) = ( A - ( A mod ( 2 ^ N ) ) ) )
62 59 14 subcld 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A - ( A mod ( 2 ^ N ) ) ) e. CC )
63 5 nncnd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. CC )
64 5 nnne0d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) =/= 0 )
65 62 63 64 divcan1d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) x. ( 2 ^ N ) ) = ( A - ( A mod ( 2 ^ N ) ) ) )
66 1 zred 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> A e. RR )
67 5 nnrpd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( 2 ^ N ) e. RR+ )
68 moddiffl 
 |-  ( ( A e. RR /\ ( 2 ^ N ) e. RR+ ) -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) = ( |_ ` ( A / ( 2 ^ N ) ) ) )
69 66 67 68 syl2anc 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) = ( |_ ` ( A / ( 2 ^ N ) ) ) )
70 69 oveq1d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( ( A - ( A mod ( 2 ^ N ) ) ) / ( 2 ^ N ) ) x. ( 2 ^ N ) ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) )
71 61 65 70 3eqtr2d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( A + -u ( A mod ( 2 ^ N ) ) ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) )
72 60 71 eqtrd 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( -u ( A mod ( 2 ^ N ) ) + A ) = ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) )
73 72 fveq2d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( bits ` ( -u ( A mod ( 2 ^ N ) ) + A ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) )
74 10 58 73 3eqtr3d 
 |-  ( ( A e. ZZ /\ N e. NN0 ) -> ( ( bits ` A ) i^i ( ZZ>= ` N ) ) = ( bits ` ( ( |_ ` ( A / ( 2 ^ N ) ) ) x. ( 2 ^ N ) ) ) )