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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) } = ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpll ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 2 ∈ ℕ )
4 simplr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
5 3 4 nnexpcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
6 5 nnzd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℤ )
7 dvdsmul2 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℤ ) → ( 2 ↑ 𝑁 ) ∥ ( 𝐴 · ( 2 ↑ 𝑁 ) ) )
8 1 6 7 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∥ ( 𝐴 · ( 2 ↑ 𝑁 ) ) )
9 1 6 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 · ( 2 ↑ 𝑁 ) ) ∈ ℤ )
10 bitsuz ⊢ ( ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) ) )
11 9 4 10 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 ↑ 𝑁 ) ∥ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) ) )
12 8 11 mpbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
13 12 sseld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) → 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
14 uznn0sub ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑛 − 𝑁 ) ∈ ℕ0 )
15 13 14 syl6 ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) → ( 𝑛 − 𝑁 ) ∈ ℕ0 ) )
16 bitsss ⊢ ( bits ‘ 𝐴 ) ⊆ ℕ0
17 16 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( bits ‘ 𝐴 ) ⊆ ℕ0 )
18 17 sseld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) → ( 𝑛 − 𝑁 ) ∈ ℕ0 ) )
19 2cnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 2 ∈ ℂ )
20 2 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 2 ∈ ℕ )
21 20 nnne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 2 ≠ 0 )
22 simplr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
23 22 nn0zd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 𝑁 ∈ ℤ )
24 simprl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 𝑛 ∈ ℕ0 )
25 24 nn0zd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 𝑛 ∈ ℤ )
26 19 21 23 25 expsubd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ ( 𝑛 − 𝑁 ) ) = ( ( 2 ↑ 𝑛 ) / ( 2 ↑ 𝑁 ) ) )
27 26 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) = ( 𝐴 / ( ( 2 ↑ 𝑛 ) / ( 2 ↑ 𝑁 ) ) ) )
28 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℤ )
29 28 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
30 29 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → 𝐴 ∈ ℂ )
31 20 24 nnexpcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
32 31 nncnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
33 20 22 nnexpcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
34 33 nncnd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
35 31 nnne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
36 33 nnne0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ↑ 𝑁 ) ≠ 0 )
37 30 32 34 35 36 divdiv2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 𝐴 / ( ( 2 ↑ 𝑛 ) / ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) )
38 27 37 eqtr2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) = ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) )
39 38 fveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( ⌊ ‘ ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) ) )
40 39 breq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 2 ∥ ( ⌊ ‘ ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) ) ↔ 2 ∥ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) ) ) )
41 40 notbid ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( ¬ 2 ∥ ( ⌊ ‘ ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) ) ) )
42 9 adantrr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 𝐴 · ( 2 ↑ 𝑁 ) ) ∈ ℤ )
43 bitsval2 ⊢ ( ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) ) ) )
44 42 24 43 syl2anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( ( 𝐴 · ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑛 ) ) ) ) )
45 bitsval2 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) → ( ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) ) ) )
46 45 ad2ant2rl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑛 − 𝑁 ) ) ) ) ) )
47 41 44 46 3bitr4d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 − 𝑁 ) ∈ ℕ0 ) ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ↔ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) ) )
48 47 expr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 − 𝑁 ) ∈ ℕ0 → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ↔ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) ) ) )
49 15 18 48 pm5.21ndd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 ∈ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ↔ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) ) )
50 49 rabbi2dva ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ℕ0 ∩ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ) = { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) } )
51 bitsss ⊢ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0
52 sseqin2 ⊢ ( ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ⊆ ℕ0 ↔ ( ℕ0 ∩ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ) = ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) )
53 51 52 mpbi ⊢ ( ℕ0 ∩ ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) ) = ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) )
54 50 53 eqtr3di ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → { 𝑛 ∈ ℕ0 ∣ ( 𝑛 − 𝑁 ) ∈ ( bits ‘ 𝐴 ) } = ( bits ‘ ( 𝐴 · ( 2 ↑ 𝑁 ) ) ) )