bitsres

Description: Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016)

		Ref	Expression
	Assertion	bitsres	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap ℤ_{\geq N} = bits (⌊\frac{A}{2^{N}}⌋ 2^{N})$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℤ$
2		2nn	$⊢ 2 \in ℕ$
3	2	a1i	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2 \in ℕ$
4		simpr	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
5	3 4	nnexpcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℕ$
6	1 5	zmodcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \mod 2^{N} \in ℕ_{0}$
7	6	nn0zd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \mod 2^{N} \in ℤ$
8	7	znegcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) \in ℤ$
9		sadadd	$⊢ (- (A \mod 2^{N}) \in ℤ \land A \in ℤ) \to bits (- (A \mod 2^{N})) sadd bits (A) = bits (- (A \mod 2^{N}) + A)$
10	8 1 9	syl2anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N})) sadd bits (A) = bits (- (A \mod 2^{N}) + A)$
11		sadadd	$⊢ (- (A \mod 2^{N}) \in ℤ \land A \mod 2^{N} \in ℤ) \to bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N}) = bits (- (A \mod 2^{N}) + (A \mod 2^{N}))$
12	8 7 11	syl2anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N}) = bits (- (A \mod 2^{N}) + (A \mod 2^{N}))$
13	8	zcnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) \in ℂ$
14	7	zcnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \mod 2^{N} \in ℂ$
15	13 14	addcomd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) + (A \mod 2^{N}) = (A \mod 2^{N}) + (- (A \mod 2^{N}))$
16	14	negidd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (A \mod 2^{N}) + (- (A \mod 2^{N})) = 0$
17	15 16	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) + (A \mod 2^{N}) = 0$
18	17	fveq2d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N}) + (A \mod 2^{N})) = bits (0)$
19		0bits	$⊢ bits (0) = \emptyset$
20	18 19	eqtrdi	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N}) + (A \mod 2^{N})) = \emptyset$
21	12 20	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N}) = \emptyset$
22	21	oveq1d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N})) sadd (bits (A) \cap ℤ_{\geq N}) = \emptyset sadd (bits (A) \cap ℤ_{\geq N})$
23		bitsss	$⊢ bits (- (A \mod 2^{N})) \subseteq ℕ_{0}$
24		bitsss	$⊢ bits (A \mod 2^{N}) \subseteq ℕ_{0}$
25		inss1	$⊢ bits (A) \cap ℤ_{\geq N} \subseteq bits (A)$
26		bitsss	$⊢ bits (A) \subseteq ℕ_{0}$
27	26	a1i	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \subseteq ℕ_{0}$
28	25 27	sstrid	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap ℤ_{\geq N} \subseteq ℕ_{0}$
29		sadass	$⊢ (bits (- (A \mod 2^{N})) \subseteq ℕ_{0} \land bits (A \mod 2^{N}) \subseteq ℕ_{0} \land bits (A) \cap ℤ_{\geq N} \subseteq ℕ_{0}) \to (bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N})) sadd (bits (A) \cap ℤ_{\geq N}) = bits (- (A \mod 2^{N})) sadd (bits (A \mod 2^{N}) sadd (bits (A) \cap ℤ_{\geq N}))$
30	23 24 28 29	mp3an12i	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N})) sadd (bits (A) \cap ℤ_{\geq N}) = bits (- (A \mod 2^{N})) sadd (bits (A \mod 2^{N}) sadd (bits (A) \cap ℤ_{\geq N}))$
31		bitsmod	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A \mod 2^{N}) = bits (A) \cap (0 ..^N)$
32	31	oveq1d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A \mod 2^{N}) sadd (bits (A) \cap ℤ_{\geq N}) = (bits (A) \cap (0 ..^N)) sadd (bits (A) \cap ℤ_{\geq N})$
33		inss1	$⊢ bits (A) \cap (0 ..^N) \subseteq bits (A)$
34	33 27	sstrid	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap (0 ..^N) \subseteq ℕ_{0}$
35		fzouzdisj	$⊢ (0 ..^N) \cap ℤ_{\geq N} = \emptyset$
36	35	ineq2i	$⊢ bits (A) \cap ((0 ..^N) \cap ℤ_{\geq N}) = bits (A) \cap \emptyset$
37		inindi	$⊢ bits (A) \cap ((0 ..^N) \cap ℤ_{\geq N}) = (bits (A) \cap (0 ..^N)) \cap (bits (A) \cap ℤ_{\geq N})$
38		in0	$⊢ bits (A) \cap \emptyset = \emptyset$
39	36 37 38	3eqtr3i	$⊢ (bits (A) \cap (0 ..^N)) \cap (bits (A) \cap ℤ_{\geq N}) = \emptyset$
40	39	a1i	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (A) \cap (0 ..^N)) \cap (bits (A) \cap ℤ_{\geq N}) = \emptyset$
41	34 28 40	saddisj	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (A) \cap (0 ..^N)) sadd (bits (A) \cap ℤ_{\geq N}) = (bits (A) \cap (0 ..^N)) \cup (bits (A) \cap ℤ_{\geq N})$
42		indi	$⊢ bits (A) \cap ((0 ..^N) \cup ℤ_{\geq N}) = (bits (A) \cap (0 ..^N)) \cup (bits (A) \cap ℤ_{\geq N})$
43	41 42	eqtr4di	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (A) \cap (0 ..^N)) sadd (bits (A) \cap ℤ_{\geq N}) = bits (A) \cap ((0 ..^N) \cup ℤ_{\geq N})$
44		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
45	4 44	eleqtrdi	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
46		fzouzsplit	$⊢ N \in ℤ_{\geq 0} \to ℤ_{\geq 0} = (0 ..^N) \cup ℤ_{\geq N}$
47	45 46	syl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to ℤ_{\geq 0} = (0 ..^N) \cup ℤ_{\geq N}$
48	44 47	syl5eq	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to ℕ_{0} = (0 ..^N) \cup ℤ_{\geq N}$
49	26 48	sseqtrid	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \subseteq (0 ..^N) \cup ℤ_{\geq N}$
50		df-ss	$⊢ bits (A) \subseteq (0 ..^N) \cup ℤ_{\geq N} \leftrightarrow bits (A) \cap ((0 ..^N) \cup ℤ_{\geq N}) = bits (A)$
51	49 50	sylib	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap ((0 ..^N) \cup ℤ_{\geq N}) = bits (A)$
52	43 51	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (A) \cap (0 ..^N)) sadd (bits (A) \cap ℤ_{\geq N}) = bits (A)$
53	32 52	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A \mod 2^{N}) sadd (bits (A) \cap ℤ_{\geq N}) = bits (A)$
54	53	oveq2d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N})) sadd (bits (A \mod 2^{N}) sadd (bits (A) \cap ℤ_{\geq N})) = bits (- (A \mod 2^{N})) sadd bits (A)$
55	30 54	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (bits (- (A \mod 2^{N})) sadd bits (A \mod 2^{N})) sadd (bits (A) \cap ℤ_{\geq N}) = bits (- (A \mod 2^{N})) sadd bits (A)$
56		sadid2	$⊢ bits (A) \cap ℤ_{\geq N} \subseteq ℕ_{0} \to \emptyset sadd (bits (A) \cap ℤ_{\geq N}) = bits (A) \cap ℤ_{\geq N}$
57	28 56	syl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to \emptyset sadd (bits (A) \cap ℤ_{\geq N}) = bits (A) \cap ℤ_{\geq N}$
58	22 55 57	3eqtr3d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N})) sadd bits (A) = bits (A) \cap ℤ_{\geq N}$
59	1	zcnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℂ$
60	13 59	addcomd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) + A = A + (- (A \mod 2^{N}))$
61	59 14	negsubd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A + (- (A \mod 2^{N})) = A - (A \mod 2^{N})$
62	59 14	subcld	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A - (A \mod 2^{N}) \in ℂ$
63	5	nncnd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℂ$
64	5	nnne0d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \neq 0$
65	62 63 64	divcan1d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (\frac{A - (A \mod 2^{N})}{2^{N}}) 2^{N} = A - (A \mod 2^{N})$
66	1	zred	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A \in ℝ$
67	5	nnrpd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to 2^{N} \in ℝ^{+}$
68		moddiffl	$⊢ (A \in ℝ \land 2^{N} \in ℝ^{+}) \to \frac{A - (A \mod 2^{N})}{2^{N}} = ⌊\frac{A}{2^{N}}⌋$
69	66 67 68	syl2anc	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to \frac{A - (A \mod 2^{N})}{2^{N}} = ⌊\frac{A}{2^{N}}⌋$
70	69	oveq1d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to (\frac{A - (A \mod 2^{N})}{2^{N}}) 2^{N} = ⌊\frac{A}{2^{N}}⌋ 2^{N}$
71	61 65 70	3eqtr2d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A + (- (A \mod 2^{N})) = ⌊\frac{A}{2^{N}}⌋ 2^{N}$
72	60 71	eqtrd	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to - (A \mod 2^{N}) + A = ⌊\frac{A}{2^{N}}⌋ 2^{N}$
73	72	fveq2d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (- (A \mod 2^{N}) + A) = bits (⌊\frac{A}{2^{N}}⌋ 2^{N})$
74	10 58 73	3eqtr3d	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to bits (A) \cap ℤ_{\geq N} = bits (⌊\frac{A}{2^{N}}⌋ 2^{N})$

Metamath Proof Explorer

Theorem bitsres

Proof