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 ↑ 𝑁 ) ) ) )