bitscmp

Description: The bit complement of N is -u N - 1 . (Thus, by bitsfi , all negative numbers have cofinite bits representations.) (Contributed by Mario Carneiro, 5-Sep-2016)

		Ref	Expression
	Assertion	bitscmp	$⊢ N \in ℤ \to ℕ_{0} ∖ bits (N) = bits (- N - 1)$

Proof

Step	Hyp	Ref	Expression
1		bitsval2	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (m \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{m}}⌋)$
2		2z	$⊢ 2 \in ℤ$
3	2	a1i	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2 \in ℤ$
4		simpl	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to N \in ℤ$
5	4	zred	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to N \in ℝ$
6		2nn	$⊢ 2 \in ℕ$
7	6	a1i	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2 \in ℕ$
8		simpr	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to m \in ℕ_{0}$
9	7 8	nnexpcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} \in ℕ$
10	5 9	nndivred	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{N}{2^{m}} \in ℝ$
11	10	flcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{N}{2^{m}}⌋ \in ℤ$
12		dvdsnegb	$⊢ (2 \in ℤ \land ⌊\frac{N}{2^{m}}⌋ \in ℤ) \to (2 ∥ ⌊\frac{N}{2^{m}}⌋ \leftrightarrow 2 ∥ (- ⌊\frac{N}{2^{m}}⌋))$
13	3 11 12	syl2anc	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (2 ∥ ⌊\frac{N}{2^{m}}⌋ \leftrightarrow 2 ∥ (- ⌊\frac{N}{2^{m}}⌋))$
14	13	notbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\neg 2 ∥ ⌊\frac{N}{2^{m}}⌋ \leftrightarrow \neg 2 ∥ (- ⌊\frac{N}{2^{m}}⌋))$
15	11	znegcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ \in ℤ$
16		oddm1even	$⊢ - ⌊\frac{N}{2^{m}}⌋ \in ℤ \to (\neg 2 ∥ (- ⌊\frac{N}{2^{m}}⌋) \leftrightarrow 2 ∥ (- ⌊\frac{N}{2^{m}}⌋ - 1))$
17	15 16	syl	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\neg 2 ∥ (- ⌊\frac{N}{2^{m}}⌋) \leftrightarrow 2 ∥ (- ⌊\frac{N}{2^{m}}⌋ - 1))$
18		flltp1	$⊢ \frac{N}{2^{m}} \in ℝ \to \frac{N}{2^{m}} < ⌊\frac{N}{2^{m}}⌋ + 1$
19	10 18	syl	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{N}{2^{m}} < ⌊\frac{N}{2^{m}}⌋ + 1$
20	11	zred	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{N}{2^{m}}⌋ \in ℝ$
21		1red	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 1 \in ℝ$
22	20 21	readdcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{N}{2^{m}}⌋ + 1 \in ℝ$
23	10 22	ltnegd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\frac{N}{2^{m}} < ⌊\frac{N}{2^{m}}⌋ + 1 \leftrightarrow - (⌊\frac{N}{2^{m}}⌋ + 1) < - \frac{N}{2^{m}})$
24	19 23	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - (⌊\frac{N}{2^{m}}⌋ + 1) < - \frac{N}{2^{m}}$
25	20	recnd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{N}{2^{m}}⌋ \in ℂ$
26	21	recnd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 1 \in ℂ$
27	25 26	negdi2d	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - (⌊\frac{N}{2^{m}}⌋ + 1) = - ⌊\frac{N}{2^{m}}⌋ - 1$
28	5	recnd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to N \in ℂ$
29	9	nncnd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} \in ℂ$
30	9	nnne0d	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} \neq 0$
31	28 29 30	divnegd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - \frac{N}{2^{m}} = \frac{- N}{2^{m}}$
32	24 27 31	3brtr3d	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ - 1 < \frac{- N}{2^{m}}$
33		1zzd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 1 \in ℤ$
34	15 33	zsubcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ - 1 \in ℤ$
35	34	zred	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ - 1 \in ℝ$
36	5	renegcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - N \in ℝ$
37	9	nnrpd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} \in ℝ^{+}$
38	35 36 37	ltmuldivd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ((- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} < - N \leftrightarrow - ⌊\frac{N}{2^{m}}⌋ - 1 < \frac{- N}{2^{m}})$
39	32 38	mpbird	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} < - N$
40	9	nnzd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} \in ℤ$
41	34 40	zmulcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \in ℤ$
42	4	znegcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - N \in ℤ$
43		zltlem1	$⊢ ((- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \in ℤ \land - N \in ℤ) \to ((- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} < - N \leftrightarrow (- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \leq - N - 1)$
44	41 42 43	syl2anc	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ((- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} < - N \leftrightarrow (- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \leq - N - 1)$
45	39 44	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \leq - N - 1$
46	36 21	resubcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - N - 1 \in ℝ$
47	35 46 37	lemuldivd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ((- ⌊\frac{N}{2^{m}}⌋ - 1) 2^{m} \leq - N - 1 \leftrightarrow - ⌊\frac{N}{2^{m}}⌋ - 1 \leq \frac{- N - 1}{2^{m}})$
48	45 47	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ - 1 \leq \frac{- N - 1}{2^{m}}$
49		flle	$⊢ \frac{N}{2^{m}} \in ℝ \to ⌊\frac{N}{2^{m}}⌋ \leq \frac{N}{2^{m}}$
50	10 49	syl	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{N}{2^{m}}⌋ \leq \frac{N}{2^{m}}$
51	20 10	lenegd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (⌊\frac{N}{2^{m}}⌋ \leq \frac{N}{2^{m}} \leftrightarrow - \frac{N}{2^{m}} \leq - ⌊\frac{N}{2^{m}}⌋)$
52	50 51	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - \frac{N}{2^{m}} \leq - ⌊\frac{N}{2^{m}}⌋$
53	31 52	eqbrtrrd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{- N}{2^{m}} \leq - ⌊\frac{N}{2^{m}}⌋$
54	20	renegcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ \in ℝ$
55	36 54 37	ledivmuld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\frac{- N}{2^{m}} \leq - ⌊\frac{N}{2^{m}}⌋ \leftrightarrow - N \leq 2^{m} (- ⌊\frac{N}{2^{m}}⌋))$
56	53 55	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - N \leq 2^{m} (- ⌊\frac{N}{2^{m}}⌋)$
57	40 15	zmulcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to 2^{m} (- ⌊\frac{N}{2^{m}}⌋) \in ℤ$
58		zlem1lt	$⊢ (- N \in ℤ \land 2^{m} (- ⌊\frac{N}{2^{m}}⌋) \in ℤ) \to (- N \leq 2^{m} (- ⌊\frac{N}{2^{m}}⌋) \leftrightarrow - N - 1 < 2^{m} (- ⌊\frac{N}{2^{m}}⌋))$
59	42 57 58	syl2anc	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (- N \leq 2^{m} (- ⌊\frac{N}{2^{m}}⌋) \leftrightarrow - N - 1 < 2^{m} (- ⌊\frac{N}{2^{m}}⌋))$
60	56 59	mpbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - N - 1 < 2^{m} (- ⌊\frac{N}{2^{m}}⌋)$
61	46 54 37	ltdivmuld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\frac{- N - 1}{2^{m}} < - ⌊\frac{N}{2^{m}}⌋ \leftrightarrow - N - 1 < 2^{m} (- ⌊\frac{N}{2^{m}}⌋))$
62	60 61	mpbird	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{- N - 1}{2^{m}} < - ⌊\frac{N}{2^{m}}⌋$
63	25	negcld	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to - ⌊\frac{N}{2^{m}}⌋ \in ℂ$
64	63 26	npcand	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (- ⌊\frac{N}{2^{m}}⌋) - 1 + 1 = - ⌊\frac{N}{2^{m}}⌋$
65	62 64	breqtrrd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{- N - 1}{2^{m}} < (- ⌊\frac{N}{2^{m}}⌋) - 1 + 1$
66	46 9	nndivred	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to \frac{- N - 1}{2^{m}} \in ℝ$
67		flbi	$⊢ (\frac{- N - 1}{2^{m}} \in ℝ \land - ⌊\frac{N}{2^{m}}⌋ - 1 \in ℤ) \to (⌊\frac{- N - 1}{2^{m}}⌋ = - ⌊\frac{N}{2^{m}}⌋ - 1 \leftrightarrow (- ⌊\frac{N}{2^{m}}⌋ - 1 \leq \frac{- N - 1}{2^{m}} \land \frac{- N - 1}{2^{m}} < (- ⌊\frac{N}{2^{m}}⌋) - 1 + 1))$
68	66 34 67	syl2anc	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (⌊\frac{- N - 1}{2^{m}}⌋ = - ⌊\frac{N}{2^{m}}⌋ - 1 \leftrightarrow (- ⌊\frac{N}{2^{m}}⌋ - 1 \leq \frac{- N - 1}{2^{m}} \land \frac{- N - 1}{2^{m}} < (- ⌊\frac{N}{2^{m}}⌋) - 1 + 1))$
69	48 65 68	mpbir2and	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to ⌊\frac{- N - 1}{2^{m}}⌋ = - ⌊\frac{N}{2^{m}}⌋ - 1$
70	69	breq2d	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋ \leftrightarrow 2 ∥ (- ⌊\frac{N}{2^{m}}⌋ - 1))$
71	17 70	bitr4d	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\neg 2 ∥ (- ⌊\frac{N}{2^{m}}⌋) \leftrightarrow 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)$
72	1 14 71	3bitrd	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (m \in bits (N) \leftrightarrow 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)$
73	72	notbid	$⊢ (N \in ℤ \land m \in ℕ_{0}) \to (\neg m \in bits (N) \leftrightarrow \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)$
74	73	pm5.32da	$⊢ N \in ℤ \to ((m \in ℕ_{0} \land \neg m \in bits (N)) \leftrightarrow (m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋))$
75		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
76		1zzd	$⊢ N \in ℤ \to 1 \in ℤ$
77	75 76	zsubcld	$⊢ N \in ℤ \to - N - 1 \in ℤ$
78	77	biantrurd	$⊢ N \in ℤ \to ((m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋) \leftrightarrow (- N - 1 \in ℤ \land (m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)))$
79	74 78	bitrd	$⊢ N \in ℤ \to ((m \in ℕ_{0} \land \neg m \in bits (N)) \leftrightarrow (- N - 1 \in ℤ \land (m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)))$
80		eldif	$⊢ m \in (ℕ_{0} ∖ bits (N)) \leftrightarrow (m \in ℕ_{0} \land \neg m \in bits (N))$
81		bitsval	$⊢ m \in bits (- N - 1) \leftrightarrow (- N - 1 \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋)$
82		3anass	$⊢ (- N - 1 \in ℤ \land m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋) \leftrightarrow (- N - 1 \in ℤ \land (m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋))$
83	81 82	bitri	$⊢ m \in bits (- N - 1) \leftrightarrow (- N - 1 \in ℤ \land (m \in ℕ_{0} \land \neg 2 ∥ ⌊\frac{- N - 1}{2^{m}}⌋))$
84	79 80 83	3bitr4g	$⊢ N \in ℤ \to (m \in (ℕ_{0} ∖ bits (N)) \leftrightarrow m \in bits (- N - 1))$
85	84	eqrdv	$⊢ N \in ℤ \to ℕ_{0} ∖ bits (N) = bits (- N - 1)$

Metamath Proof Explorer

Theorem bitscmp

Proof