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