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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℕ )
4 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5 3 4 nnexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
6 1 5 zmodcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℕ0 )
7 6 nn0zd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℤ )
8 7 znegcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℤ )
9 sadadd ⊢ ( ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ 𝐴 ) ) = ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + 𝐴 ) ) )
10 8 1 9 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ 𝐴 ) ) = ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + 𝐴 ) ) )
11 sadadd ⊢ ( ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) = ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
12 8 7 11 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) = ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
13 8 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
14 7 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
15 13 14 addcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
16 14 negidd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = 0 )
17 15 16 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = 0 )
18 17 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) = ( bits ‘ 0 ) )
19 0bits ⊢ ( bits ‘ 0 ) = ∅
20 18 19 eqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) = ∅ )
21 12 20 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) = ∅ )
22 21 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ∅ sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) )
23 bitsss ⊢ ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0
24 bitsss ⊢ ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0
25 inss1 ⊢ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ( bits ‘ 𝐴 )
26 bitsss ⊢ ( bits ‘ 𝐴 ) ⊆ ℕ0
27 26 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ 𝐴 ) ⊆ ℕ0 )
28 25 27 sstrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ℕ0 )
29 sadass ⊢ ( ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0 ∧ ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0 ∧ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ℕ0 ) → ( ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) ) )
30 23 24 28 29 mp3an12i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) ) )
31 bitsmod ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) )
32 31 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) )
33 inss1 ⊢ ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( bits ‘ 𝐴 )
34 33 27 sstrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
35 fzouzdisj ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ∅
36 35 ineq2i ⊢ ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ∅ )
37 inindi ⊢ ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∩ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) )
38 in0 ⊢ ( ( bits ‘ 𝐴 ) ∩ ∅ ) = ∅
39 36 37 38 3eqtr3i ⊢ ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∩ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ∅
40 39 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∩ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ∅ )
41 34 28 40 saddisj ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∪ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) )
42 indi ⊢ ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) ∪ ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) )
43 41 42 eqtr4di ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) )
44 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
45 4 44 eleqtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
46 fzouzsplit ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )
47 45 46 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )
48 44 47 eqtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ℕ0 = ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )
49 26 48 sseqtrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ 𝐴 ) ⊆ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )
50 df-ss ⊢ ( ( bits ‘ 𝐴 ) ⊆ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ↔ ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) )
51 49 50 sylib ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( ( 0 ..^ 𝑁 ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) )
52 43 51 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ 𝐴 ) ∩ ( 0 ..^ 𝑁 ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) )
53 32 52 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( bits ‘ 𝐴 ) )
54 53 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) ) = ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ 𝐴 ) ) )
55 30 54 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ 𝐴 ) ) )
56 sadid2 ⊢ ( ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ⊆ ℕ0 → ( ∅ sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) )
57 28 56 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ∅ sadd ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) ) = ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) )
58 22 55 57 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) sadd ( bits ‘ 𝐴 ) ) = ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) )
59 1 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
60 13 59 addcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + 𝐴 ) = ( 𝐴 + - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
61 59 14 negsubd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 + - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
62 59 14 subcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ∈ ℂ )
63 5 nncnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
64 5 nnne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ≠ 0 )
65 62 63 64 divcan1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) · ( 2 ↑ 𝑁 ) ) = ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
66 1 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
67 5 nnrpd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
68 moddiffl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) )
69 66 67 68 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) )
70 69 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) · ( 2 ↑ 𝑁 ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) )
71 61 65 70 3eqtr2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 + - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) )
72 60 71 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + 𝐴 ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) )
73 72 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( bits ‘ ( - ( 𝐴 mod ( 2 ↑ 𝑁 ) ) + 𝐴 ) ) = ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) )
74 10 58 73 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( bits ‘ 𝐴 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( bits ‘ ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) · ( 2 ↑ 𝑁 ) ) ) )