bitsmod

Description: Truncating the bit sequence after some M is equivalent to reducing the argument mod 2 ^ M . (Contributed by Mario Carneiro, 6-Sep-2016)

		Ref	Expression
	Assertion	bitsmod	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to bits (N \mod 2^{M}) = bits (N) \cap (0 ..^M)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \in ℤ$
2		2nn	$⊢ 2 \in ℕ$
3	2	a1i	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2 \in ℕ$
4		simpr	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to M \in ℕ_{0}$
5	3 4	nnexpcld	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to 2^{M} \in ℕ$
6	1 5	zmodcld	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \mod 2^{M} \in ℕ_{0}$
7	6	nn0zd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to N \mod 2^{M} \in ℤ$
8	7	biantrurd	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ((x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋) \leftrightarrow (N \mod 2^{M} \in ℤ \land (x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)))$
9	1	ad2antrr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \in ℤ$
10		simplr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x \in ℕ_{0}$
11		bitsval2	$⊢ (N \in ℤ \land x \in ℕ_{0}) \to (x \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{x}}⌋)$
12	9 10 11	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (x \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{x}}⌋)$
13		simpr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x < M$
14	13	biantrud	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (x \in bits (N) \leftrightarrow (x \in bits (N) \land x < M))$
15		2z	$⊢ 2 \in ℤ$
16	15	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 \in ℤ$
17	9	zred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \in ℝ$
18	2	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 \in ℕ$
19	18 10	nnexpcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \in ℕ$
20	17 19	nndivred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N}{2^{x}} \in ℝ$
21	20	flcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N}{2^{x}}⌋ \in ℤ$
22	7	ad2antrr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \mod 2^{M} \in ℤ$
23	22	zred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \mod 2^{M} \in ℝ$
24	23 19	nndivred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N \mod 2^{M}}{2^{x}} \in ℝ$
25	24	flcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \in ℤ$
26	19	nnzd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \in ℤ$
27	26 16	zmulcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \cdot 2 \in ℤ$
28	5	ad2antrr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{M} \in ℕ$
29	28	nnzd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{M} \in ℤ$
30	9 22	zsubcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N - (N \mod 2^{M}) \in ℤ$
31		2cnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 \in ℂ$
32	31 10	expp1d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x + 1} = 2^{x} \cdot 2$
33		1nn0	$⊢ 1 \in ℕ_{0}$
34	33	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 1 \in ℕ_{0}$
35	10 34	nn0addcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x + 1 \in ℕ_{0}$
36	35	nn0zd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x + 1 \in ℤ$
37		simplr	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to M \in ℕ_{0}$
38	37	adantr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to M \in ℕ_{0}$
39	38	nn0zd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to M \in ℤ$
40		nn0ltp1le	$⊢ (x \in ℕ_{0} \land M \in ℕ_{0}) \to (x < M \leftrightarrow x + 1 \leq M)$
41	10 38 40	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (x < M \leftrightarrow x + 1 \leq M)$
42	13 41	mpbid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x + 1 \leq M$
43		eluz2	$⊢ M \in ℤ_{\geq (x + 1)} \leftrightarrow (x + 1 \in ℤ \land M \in ℤ \land x + 1 \leq M)$
44	36 39 42 43	syl3anbrc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to M \in ℤ_{\geq (x + 1)}$
45		dvdsexp	$⊢ (2 \in ℤ \land x + 1 \in ℕ_{0} \land M \in ℤ_{\geq (x + 1)}) \to 2^{x + 1} ∥ 2^{M}$
46	16 35 44 45	syl3anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x + 1} ∥ 2^{M}$
47	32 46	eqbrtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \cdot 2 ∥ 2^{M}$
48	28	nnrpd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{M} \in ℝ^{+}$
49		moddifz	$⊢ (N \in ℝ \land 2^{M} \in ℝ^{+}) \to \frac{N - (N \mod 2^{M})}{2^{M}} \in ℤ$
50	17 48 49	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N - (N \mod 2^{M})}{2^{M}} \in ℤ$
51		2ne0	$⊢ 2 \neq 0$
52	51	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 \neq 0$
53	31 52 39	expne0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{M} \neq 0$
54		dvdsval2	$⊢ (2^{M} \in ℤ \land 2^{M} \neq 0 \land N - (N \mod 2^{M}) \in ℤ) \to (2^{M} ∥ (N - (N \mod 2^{M})) \leftrightarrow \frac{N - (N \mod 2^{M})}{2^{M}} \in ℤ)$
55	29 53 30 54	syl3anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (2^{M} ∥ (N - (N \mod 2^{M})) \leftrightarrow \frac{N - (N \mod 2^{M})}{2^{M}} \in ℤ)$
56	50 55	mpbird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{M} ∥ (N - (N \mod 2^{M}))$
57	27 29 30 47 56	dvdstrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \cdot 2 ∥ (N - (N \mod 2^{M}))$
58	30	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N - (N \mod 2^{M}) \in ℂ$
59	19	nncnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \in ℂ$
60	10	nn0zd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x \in ℤ$
61	31 52 60	expne0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \neq 0$
62	58 59 61	divcan2d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} (\frac{N - (N \mod 2^{M})}{2^{x}}) = N - (N \mod 2^{M})$
63	57 62	breqtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} \cdot 2 ∥ 2^{x} (\frac{N - (N \mod 2^{M})}{2^{x}})$
64	10	nn0red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x \in ℝ$
65	38	nn0red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to M \in ℝ$
66	64 65 13	ltled	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to x \leq M$
67		eluz2	$⊢ M \in ℤ_{\geq x} \leftrightarrow (x \in ℤ \land M \in ℤ \land x \leq M)$
68	60 39 66 67	syl3anbrc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to M \in ℤ_{\geq x}$
69		dvdsexp	$⊢ (2 \in ℤ \land x \in ℕ_{0} \land M \in ℤ_{\geq x}) \to 2^{x} ∥ 2^{M}$
70	16 10 68 69	syl3anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} ∥ 2^{M}$
71	26 29 30 70 56	dvdstrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2^{x} ∥ (N - (N \mod 2^{M}))$
72		dvdsval2	$⊢ (2^{x} \in ℤ \land 2^{x} \neq 0 \land N - (N \mod 2^{M}) \in ℤ) \to (2^{x} ∥ (N - (N \mod 2^{M})) \leftrightarrow \frac{N - (N \mod 2^{M})}{2^{x}} \in ℤ)$
73	26 61 30 72	syl3anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (2^{x} ∥ (N - (N \mod 2^{M})) \leftrightarrow \frac{N - (N \mod 2^{M})}{2^{x}} \in ℤ)$
74	71 73	mpbid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N - (N \mod 2^{M})}{2^{x}} \in ℤ$
75		dvdscmulr	$⊢ (2 \in ℤ \land \frac{N - (N \mod 2^{M})}{2^{x}} \in ℤ \land (2^{x} \in ℤ \land 2^{x} \neq 0)) \to (2^{x} \cdot 2 ∥ 2^{x} (\frac{N - (N \mod 2^{M})}{2^{x}}) \leftrightarrow 2 ∥ (\frac{N - (N \mod 2^{M})}{2^{x}}))$
76	16 74 26 61 75	syl112anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (2^{x} \cdot 2 ∥ 2^{x} (\frac{N - (N \mod 2^{M})}{2^{x}}) \leftrightarrow 2 ∥ (\frac{N - (N \mod 2^{M})}{2^{x}}))$
77	63 76	mpbid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 ∥ (\frac{N - (N \mod 2^{M})}{2^{x}})$
78	25	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \in ℂ$
79	74	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N - (N \mod 2^{M})}{2^{x}} \in ℂ$
80	22	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \mod 2^{M} \in ℂ$
81	9	zcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to N \in ℂ$
82	80 81	pncan3d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (N \mod 2^{M}) + N - (N \mod 2^{M}) = N$
83	82	oveq1d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{(N \mod 2^{M}) + N - (N \mod 2^{M})}{2^{x}} = \frac{N}{2^{x}}$
84	80 58 59 61	divdird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{(N \mod 2^{M}) + N - (N \mod 2^{M})}{2^{x}} = (\frac{N \mod 2^{M}}{2^{x}}) + (\frac{N - (N \mod 2^{M})}{2^{x}})$
85	83 84	eqtr3d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to \frac{N}{2^{x}} = (\frac{N \mod 2^{M}}{2^{x}}) + (\frac{N - (N \mod 2^{M})}{2^{x}})$
86	85	fveq2d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N}{2^{x}}⌋ = ⌊(\frac{N \mod 2^{M}}{2^{x}}) + (\frac{N - (N \mod 2^{M})}{2^{x}})⌋$
87		fladdz	$⊢ (\frac{N \mod 2^{M}}{2^{x}} \in ℝ \land \frac{N - (N \mod 2^{M})}{2^{x}} \in ℤ) \to ⌊(\frac{N \mod 2^{M}}{2^{x}}) + (\frac{N - (N \mod 2^{M})}{2^{x}})⌋ = ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ + (\frac{N - (N \mod 2^{M})}{2^{x}})$
88	24 74 87	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊(\frac{N \mod 2^{M}}{2^{x}}) + (\frac{N - (N \mod 2^{M})}{2^{x}})⌋ = ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ + (\frac{N - (N \mod 2^{M})}{2^{x}})$
89	86 88	eqtrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N}{2^{x}}⌋ = ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ + (\frac{N - (N \mod 2^{M})}{2^{x}})$
90	78 79 89	mvrladdd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ⌊\frac{N}{2^{x}}⌋ - ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ = \frac{N - (N \mod 2^{M})}{2^{x}}$
91	77 90	breqtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to 2 ∥ (⌊\frac{N}{2^{x}}⌋ - ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
92		dvdssub2	$⊢ ((2 \in ℤ \land ⌊\frac{N}{2^{x}}⌋ \in ℤ \land ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \in ℤ) \land 2 ∥ (⌊\frac{N}{2^{x}}⌋ - ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)) \to (2 ∥ ⌊\frac{N}{2^{x}}⌋ \leftrightarrow 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
93	16 21 25 91 92	syl31anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (2 ∥ ⌊\frac{N}{2^{x}}⌋ \leftrightarrow 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
94	93	notbid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to (\neg 2 ∥ ⌊\frac{N}{2^{x}}⌋ \leftrightarrow \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
95	12 14 94	3bitr3d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land x < M) \to ((x \in bits (N) \land x < M) \leftrightarrow \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
96		z0even	$⊢ 2 ∥ 0$
97	1	ad2antrr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \in ℤ$
98	97	zred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \in ℝ$
99		2rp	$⊢ 2 \in ℝ^{+}$
100	99	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2 \in ℝ^{+}$
101	37	nn0zd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to M \in ℤ$
102	101	adantr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to M \in ℤ$
103	100 102	rpexpcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{M} \in ℝ^{+}$
104	98 103	modcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \mod 2^{M} \in ℝ$
105		simplr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to x \in ℕ_{0}$
106	105	nn0zd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to x \in ℤ$
107	100 106	rpexpcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{x} \in ℝ^{+}$
108	6	ad2antrr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \mod 2^{M} \in ℕ_{0}$
109	108	nn0ge0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 0 \leq N \mod 2^{M}$
110	104 107 109	divge0d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 0 \leq \frac{N \mod 2^{M}}{2^{x}}$
111	103	rpred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{M} \in ℝ$
112	107	rpred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{x} \in ℝ$
113		modlt	$⊢ (N \in ℝ \land 2^{M} \in ℝ^{+}) \to N \mod 2^{M} < 2^{M}$
114	98 103 113	syl2anc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \mod 2^{M} < 2^{M}$
115	100	rpred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2 \in ℝ$
116		1le2	$⊢ 1 \leq 2$
117	116	a1i	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 1 \leq 2$
118	102	zred	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to M \in ℝ$
119	105	nn0red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to x \in ℝ$
120		simpr	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to \neg x < M$
121	118 119 120	nltled	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to M \leq x$
122		eluz2	$⊢ x \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land x \in ℤ \land M \leq x)$
123	102 106 121 122	syl3anbrc	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to x \in ℤ_{\geq M}$
124	115 117 123	leexp2ad	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{M} \leq 2^{x}$
125	104 111 112 114 124	ltletrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \mod 2^{M} < 2^{x}$
126	107	rpcnd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{x} \in ℂ$
127	126	mulid1d	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2^{x} \cdot 1 = 2^{x}$
128	125 127	breqtrrd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to N \mod 2^{M} < 2^{x} \cdot 1$
129		1red	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 1 \in ℝ$
130	104 129 107	ltdivmuld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to (\frac{N \mod 2^{M}}{2^{x}} < 1 \leftrightarrow N \mod 2^{M} < 2^{x} \cdot 1)$
131	128 130	mpbird	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to \frac{N \mod 2^{M}}{2^{x}} < 1$
132		1e0p1	$⊢ 1 = 0 + 1$
133	131 132	breqtrdi	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to \frac{N \mod 2^{M}}{2^{x}} < 0 + 1$
134	104 107	rerpdivcld	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to \frac{N \mod 2^{M}}{2^{x}} \in ℝ$
135		0z	$⊢ 0 \in ℤ$
136		flbi	$⊢ (\frac{N \mod 2^{M}}{2^{x}} \in ℝ \land 0 \in ℤ) \to (⌊\frac{N \mod 2^{M}}{2^{x}}⌋ = 0 \leftrightarrow (0 \leq \frac{N \mod 2^{M}}{2^{x}} \land \frac{N \mod 2^{M}}{2^{x}} < 0 + 1))$
137	134 135 136	sylancl	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to (⌊\frac{N \mod 2^{M}}{2^{x}}⌋ = 0 \leftrightarrow (0 \leq \frac{N \mod 2^{M}}{2^{x}} \land \frac{N \mod 2^{M}}{2^{x}} < 0 + 1))$
138	110 133 137	mpbir2and	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ = 0$
139	96 138	breqtrrid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋$
140	120	intnand	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to \neg (x \in bits (N) \land x < M)$
141	139 140	2thd	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to (2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \leftrightarrow \neg (x \in bits (N) \land x < M))$
142	141	con2bid	$⊢ (((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \land \neg x < M) \to ((x \in bits (N) \land x < M) \leftrightarrow \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
143	95 142	pm2.61dan	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to ((x \in bits (N) \land x < M) \leftrightarrow \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
144	101	biantrurd	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to ((x \in bits (N) \land x < M) \leftrightarrow (M \in ℤ \land (x \in bits (N) \land x < M)))$
145	143 144	bitr3d	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to (\neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \leftrightarrow (M \in ℤ \land (x \in bits (N) \land x < M)))$
146		an12	$⊢ (M \in ℤ \land (x \in bits (N) \land x < M)) \leftrightarrow (x \in bits (N) \land (M \in ℤ \land x < M))$
147	145 146	bitrdi	$⊢ ((N \in ℤ \land M \in ℕ_{0}) \land x \in ℕ_{0}) \to (\neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋ \leftrightarrow (x \in bits (N) \land (M \in ℤ \land x < M)))$
148	147	pm5.32da	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ((x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋) \leftrightarrow (x \in ℕ_{0} \land (x \in bits (N) \land (M \in ℤ \land x < M))))$
149	8 148	bitr3d	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ((N \mod 2^{M} \in ℤ \land (x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)) \leftrightarrow (x \in ℕ_{0} \land (x \in bits (N) \land (M \in ℤ \land x < M))))$
150		3anass	$⊢ (N \mod 2^{M} \in ℤ \land x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋) \leftrightarrow (N \mod 2^{M} \in ℤ \land (x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋))$
151		elfzo2	$⊢ x \in (0 ..^M) \leftrightarrow (x \in ℤ_{\geq 0} \land M \in ℤ \land x < M)$
152		elnn0uz	$⊢ x \in ℕ_{0} \leftrightarrow x \in ℤ_{\geq 0}$
153	152	3anbi1i	$⊢ (x \in ℕ_{0} \land M \in ℤ \land x < M) \leftrightarrow (x \in ℤ_{\geq 0} \land M \in ℤ \land x < M)$
154		3anass	$⊢ (x \in ℕ_{0} \land M \in ℤ \land x < M) \leftrightarrow (x \in ℕ_{0} \land (M \in ℤ \land x < M))$
155	151 153 154	3bitr2i	$⊢ x \in (0 ..^M) \leftrightarrow (x \in ℕ_{0} \land (M \in ℤ \land x < M))$
156	155	anbi2i	$⊢ (x \in bits (N) \land x \in (0 ..^M)) \leftrightarrow (x \in bits (N) \land (x \in ℕ_{0} \land (M \in ℤ \land x < M)))$
157		an12	$⊢ (x \in bits (N) \land (x \in ℕ_{0} \land (M \in ℤ \land x < M))) \leftrightarrow (x \in ℕ_{0} \land (x \in bits (N) \land (M \in ℤ \land x < M)))$
158	156 157	bitri	$⊢ (x \in bits (N) \land x \in (0 ..^M)) \leftrightarrow (x \in ℕ_{0} \land (x \in bits (N) \land (M \in ℤ \land x < M)))$
159	149 150 158	3bitr4g	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to ((N \mod 2^{M} \in ℤ \land x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋) \leftrightarrow (x \in bits (N) \land x \in (0 ..^M)))$
160		bitsval	$⊢ x \in bits (N \mod 2^{M}) \leftrightarrow (N \mod 2^{M} \in ℤ \land x \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{N \mod 2^{M}}{2^{x}}⌋)$
161		elin	$⊢ x \in (bits (N) \cap (0 ..^M)) \leftrightarrow (x \in bits (N) \land x \in (0 ..^M))$
162	159 160 161	3bitr4g	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to (x \in bits (N \mod 2^{M}) \leftrightarrow x \in (bits (N) \cap (0 ..^M)))$
163	162	eqrdv	$⊢ (N \in ℤ \land M \in ℕ_{0}) \to bits (N \mod 2^{M}) = bits (N) \cap (0 ..^M)$

Metamath Proof Explorer

Theorem bitsmod

Proof