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 \in ℤ \land N \in ℕ_{0}) \to \{n \in ℕ_{0} \| n - N \in bits (A)\} = bits (A 2^{N})$

Proof

Step	Hyp	Ref	Expression
1		bitsss	$⊢ bits (A 2^{N}) \subseteq ℕ_{0}$
2		sseqin2	$⊢ bits (A 2^{N}) \subseteq ℕ_{0} \leftrightarrow ℕ_{0} \cap bits (A 2^{N}) = bits (A 2^{N})$
3	1 2	mpbi	$⊢ ℕ_{0} \cap bits (A 2^{N}) = bits (A 2^{N})$
4		simpll	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to A \in ℤ$
5		2nn	$⊢ 2 \in ℕ$
6	5	a1i	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to 2 \in ℕ$
7		simplr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to N \in ℕ_{0}$
8	6 7	nnexpcld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to 2^{N} \in ℕ$
9	8	nnzd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to 2^{N} \in ℤ$
10		dvdsmul2	$⊢ (A \in ℤ \land 2^{N} \in ℤ) \to 2^{N} ∥ A 2^{N}$
11	4 9 10	syl2anc	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to 2^{N} ∥ A 2^{N}$
12	4 9	zmulcld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to A 2^{N} \in ℤ$
13		bitsuz	$⊢ (A 2^{N} \in ℤ \land N \in ℕ_{0}) \to (2^{N} ∥ A 2^{N} \leftrightarrow bits (A 2^{N}) \subseteq ℤ_{\geq N})$
14	12 7 13	syl2anc	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (2^{N} ∥ A 2^{N} \leftrightarrow bits (A 2^{N}) \subseteq ℤ_{\geq N})$
15	11 14	mpbid	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to bits (A 2^{N}) \subseteq ℤ_{\geq N}$
16	15	sseld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (n \in bits (A 2^{N}) \to n \in ℤ_{\geq N})$
17		uznn0sub	$⊢ n \in ℤ_{\geq N} \to n - N \in ℕ_{0}$
18	16 17	syl6	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (n \in bits (A 2^{N}) \to n - N \in ℕ_{0})$
19		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
20	19	a1i	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to bits (A) \subseteq ℕ_{0}$
21	20	sseld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (n - N \in bits (A) \to n - N \in ℕ_{0})$
22		2cnd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2 \in ℂ$
23	5	a1i	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2 \in ℕ$
24	23	nnne0d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2 \neq 0$
25		simplr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to N \in ℕ_{0}$
26	25	nn0zd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to N \in ℤ$
27		simprl	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to n \in ℕ_{0}$
28	27	nn0zd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to n \in ℤ$
29	22 24 26 28	expsubd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{n - N} = \frac{2^{n}}{2^{N}}$
30	29	oveq2d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to \frac{A}{2^{n - N}} = \frac{A}{\frac{2^{n}}{2^{N}}}$
31		simpl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℤ$
32	31	zcnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℂ$
33	32	adantr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to A \in ℂ$
34	23 27	nnexpcld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{n} \in ℕ$
35	34	nncnd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{n} \in ℂ$
36	23 25	nnexpcld	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{N} \in ℕ$
37	36	nncnd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{N} \in ℂ$
38	34	nnne0d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{n} \neq 0$
39	36	nnne0d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to 2^{N} \neq 0$
40	33 35 37 38 39	divdiv2d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to \frac{A}{\frac{2^{n}}{2^{N}}} = \frac{A 2^{N}}{2^{n}}$
41	30 40	eqtr2d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to \frac{A 2^{N}}{2^{n}} = \frac{A}{2^{n - N}}$
42	41	fveq2d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to ⌊\frac{A 2^{N}}{2^{n}}⌋ = ⌊\frac{A}{2^{n - N}}⌋$
43	42	breq2d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to (2 ∥ ⌊\frac{A 2^{N}}{2^{n}}⌋ \leftrightarrow 2 ∥ ⌊\frac{A}{2^{n - N}}⌋)$
44	43	notbid	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to (\neg 2 ∥ ⌊\frac{A 2^{N}}{2^{n}}⌋ \leftrightarrow \neg 2 ∥ ⌊\frac{A}{2^{n - N}}⌋)$
45	12	adantrr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to A 2^{N} \in ℤ$
46		bitsval2	$⊢ (A 2^{N} \in ℤ \land n \in ℕ_{0}) \to (n \in bits (A 2^{N}) \leftrightarrow \neg 2 ∥ ⌊\frac{A 2^{N}}{2^{n}}⌋)$
47	45 27 46	syl2anc	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to (n \in bits (A 2^{N}) \leftrightarrow \neg 2 ∥ ⌊\frac{A 2^{N}}{2^{n}}⌋)$
48		bitsval2	$⊢ (A \in ℤ \land n - N \in ℕ_{0}) \to (n - N \in bits (A) \leftrightarrow \neg 2 ∥ ⌊\frac{A}{2^{n - N}}⌋)$
49	48	ad2ant2rl	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to (n - N \in bits (A) \leftrightarrow \neg 2 ∥ ⌊\frac{A}{2^{n - N}}⌋)$
50	44 47 49	3bitr4d	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land (n \in ℕ_{0} \land n - N \in ℕ_{0})) \to (n \in bits (A 2^{N}) \leftrightarrow n - N \in bits (A))$
51	50	expr	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (n - N \in ℕ_{0} \to (n \in bits (A 2^{N}) \leftrightarrow n - N \in bits (A)))$
52	18 21 51	pm5.21ndd	$⊢ ((A \in ℤ \land N \in ℕ_{0}) \land n \in ℕ_{0}) \to (n \in bits (A 2^{N}) \leftrightarrow n - N \in bits (A))$
53	52	rabbi2dva	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to ℕ_{0} \cap bits (A 2^{N}) = \{n \in ℕ_{0} \| n - N \in bits (A)\}$
54	3 53	syl5reqr	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to \{n \in ℕ_{0} \| n - N \in bits (A)\} = bits (A 2^{N})$

Metamath Proof Explorer

Theorem bitsshft

Proof