bitsinv1

Description: There is an explicit inverse to the bits function for nonnegative integers (which can be extended to negative integers using bitscmp ), part 1. (Contributed by Mario Carneiro, 7-Sep-2016)

		Ref	Expression
	Assertion	bitsinv1	$⊢ N \in ℕ_{0} \to \sum_{n \in bits (N)} 2^{n} = N$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 0 \to (0 ..^x) = (0 ..^0)$
2		fzo0	$⊢ (0 ..^0) = \emptyset$
3	1 2	eqtrdi	$⊢ x = 0 \to (0 ..^x) = \emptyset$
4	3	ineq2d	$⊢ x = 0 \to bits (N) \cap (0 ..^x) = bits (N) \cap \emptyset$
5		in0	$⊢ bits (N) \cap \emptyset = \emptyset$
6	4 5	eqtrdi	$⊢ x = 0 \to bits (N) \cap (0 ..^x) = \emptyset$
7	6	sumeq1d	$⊢ x = 0 \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = \sum_{n \in \emptyset} 2^{n}$
8		sum0	$⊢ \sum_{n \in \emptyset} 2^{n} = 0$
9	7 8	eqtrdi	$⊢ x = 0 \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = 0$
10		oveq2	$⊢ x = 0 \to 2^{x} = 2^{0}$
11		2cn	$⊢ 2 \in ℂ$
12		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
13	11 12	ax-mp	$⊢ 2^{0} = 1$
14	10 13	eqtrdi	$⊢ x = 0 \to 2^{x} = 1$
15	14	oveq2d	$⊢ x = 0 \to N \mod 2^{x} = N \mod 1$
16	9 15	eqeq12d	$⊢ x = 0 \to (\sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x} \leftrightarrow 0 = N \mod 1)$
17	16	imbi2d	$⊢ x = 0 \to ((N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x}) \leftrightarrow (N \in ℕ_{0} \to 0 = N \mod 1))$
18		oveq2	$⊢ x = k \to (0 ..^x) = (0 ..^k)$
19	18	ineq2d	$⊢ x = k \to bits (N) \cap (0 ..^x) = bits (N) \cap (0 ..^k)$
20	19	sumeq1d	$⊢ x = k \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n}$
21		oveq2	$⊢ x = k \to 2^{x} = 2^{k}$
22	21	oveq2d	$⊢ x = k \to N \mod 2^{x} = N \mod 2^{k}$
23	20 22	eqeq12d	$⊢ x = k \to (\sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x} \leftrightarrow \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k})$
24	23	imbi2d	$⊢ x = k \to ((N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x}) \leftrightarrow (N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k}))$
25		oveq2	$⊢ x = k + 1 \to (0 ..^x) = (0 ..^k + 1)$
26	25	ineq2d	$⊢ x = k + 1 \to bits (N) \cap (0 ..^x) = bits (N) \cap (0 ..^k + 1)$
27	26	sumeq1d	$⊢ x = k + 1 \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n}$
28		oveq2	$⊢ x = k + 1 \to 2^{x} = 2^{k + 1}$
29	28	oveq2d	$⊢ x = k + 1 \to N \mod 2^{x} = N \mod 2^{k + 1}$
30	27 29	eqeq12d	$⊢ x = k + 1 \to (\sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x} \leftrightarrow \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1})$
31	30	imbi2d	$⊢ x = k + 1 \to ((N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x}) \leftrightarrow (N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1}))$
32		oveq2	$⊢ x = N \to (0 ..^x) = (0 ..^N)$
33	32	ineq2d	$⊢ x = N \to bits (N) \cap (0 ..^x) = bits (N) \cap (0 ..^N)$
34	33	sumeq1d	$⊢ x = N \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n}$
35		oveq2	$⊢ x = N \to 2^{x} = 2^{N}$
36	35	oveq2d	$⊢ x = N \to N \mod 2^{x} = N \mod 2^{N}$
37	34 36	eqeq12d	$⊢ x = N \to (\sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x} \leftrightarrow \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n} = N \mod 2^{N})$
38	37	imbi2d	$⊢ x = N \to ((N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^x)} 2^{n} = N \mod 2^{x}) \leftrightarrow (N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n} = N \mod 2^{N}))$
39		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
40		zmod10	$⊢ N \in ℤ \to N \mod 1 = 0$
41	39 40	syl	$⊢ N \in ℕ_{0} \to N \mod 1 = 0$
42	41	eqcomd	$⊢ N \in ℕ_{0} \to 0 = N \mod 1$
43		oveq1	$⊢ \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k} \to \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} + \sum_{n \in bits (N) \cap \{k\}} 2^{n} = (N \mod 2^{k}) + \sum_{n \in bits (N) \cap \{k\}} 2^{n}$
44		fzonel	$⊢ \neg k \in (0 ..^k)$
45	44	a1i	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \neg k \in (0 ..^k)$
46		disjsn	$⊢ (0 ..^k) \cap \{k\} = \emptyset \leftrightarrow \neg k \in (0 ..^k)$
47	45 46	sylibr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (0 ..^k) \cap \{k\} = \emptyset$
48	47	ineq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to bits (N) \cap ((0 ..^k) \cap \{k\}) = bits (N) \cap \emptyset$
49		inindi	$⊢ bits (N) \cap ((0 ..^k) \cap \{k\}) = (bits (N) \cap (0 ..^k)) \cap (bits (N) \cap \{k\})$
50	48 49 5	3eqtr3g	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (bits (N) \cap (0 ..^k)) \cap (bits (N) \cap \{k\}) = \emptyset$
51		simpr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℕ_{0}$
52		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
53	51 52	eleqtrdi	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
54		fzosplitsn	$⊢ k \in ℤ_{\geq 0} \to (0 ..^k + 1) = (0 ..^k) \cup \{k\}$
55	53 54	syl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (0 ..^k + 1) = (0 ..^k) \cup \{k\}$
56	55	ineq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to bits (N) \cap (0 ..^k + 1) = bits (N) \cap ((0 ..^k) \cup \{k\})$
57		indi	$⊢ bits (N) \cap ((0 ..^k) \cup \{k\}) = (bits (N) \cap (0 ..^k)) \cup (bits (N) \cap \{k\})$
58	56 57	eqtrdi	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to bits (N) \cap (0 ..^k + 1) = (bits (N) \cap (0 ..^k)) \cup (bits (N) \cap \{k\})$
59		fzofi	$⊢ (0 ..^k + 1) \in Fin$
60		inss2	$⊢ bits (N) \cap (0 ..^k + 1) \subseteq (0 ..^k + 1)$
61		ssfi	$⊢ ((0 ..^k + 1) \in Fin \land bits (N) \cap (0 ..^k + 1) \subseteq (0 ..^k + 1)) \to bits (N) \cap (0 ..^k + 1) \in Fin$
62	59 60 61	mp2an	$⊢ bits (N) \cap (0 ..^k + 1) \in Fin$
63	62	a1i	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to bits (N) \cap (0 ..^k + 1) \in Fin$
64		2nn	$⊢ 2 \in ℕ$
65	64	a1i	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to 2 \in ℕ$
66		simpr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to n \in (bits (N) \cap (0 ..^k + 1))$
67	66	elin2d	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to n \in (0 ..^k + 1)$
68		elfzouz	$⊢ n \in (0 ..^k + 1) \to n \in ℤ_{\geq 0}$
69	67 68	syl	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to n \in ℤ_{\geq 0}$
70	69 52	eleqtrrdi	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to n \in ℕ_{0}$
71	65 70	nnexpcld	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to 2^{n} \in ℕ$
72	71	nncnd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land n \in (bits (N) \cap (0 ..^k + 1))) \to 2^{n} \in ℂ$
73	50 58 63 72	fsumsplit	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} + \sum_{n \in bits (N) \cap \{k\}} 2^{n}$
74		bitsinv1lem	$⊢ (N \in ℤ \land k \in ℕ_{0}) \to N \mod 2^{k + 1} = (N \mod 2^{k}) + if (k \in bits (N), 2^{k}, 0)$
75	39 74	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \mod 2^{k + 1} = (N \mod 2^{k}) + if (k \in bits (N), 2^{k}, 0)$
76		eqeq2	$⊢ 2^{k} = if (k \in bits (N), 2^{k}, 0) \to (\sum_{n \in bits (N) \cap \{k\}} 2^{n} = 2^{k} \leftrightarrow \sum_{n \in bits (N) \cap \{k\}} 2^{n} = if (k \in bits (N), 2^{k}, 0))$
77		eqeq2	$⊢ 0 = if (k \in bits (N), 2^{k}, 0) \to (\sum_{n \in bits (N) \cap \{k\}} 2^{n} = 0 \leftrightarrow \sum_{n \in bits (N) \cap \{k\}} 2^{n} = if (k \in bits (N), 2^{k}, 0))$
78		simpr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to k \in bits (N)$
79	78	snssd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to \{k\} \subseteq bits (N)$
80		sseqin2	$⊢ \{k\} \subseteq bits (N) \leftrightarrow bits (N) \cap \{k\} = \{k\}$
81	79 80	sylib	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to bits (N) \cap \{k\} = \{k\}$
82	81	sumeq1d	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to \sum_{n \in bits (N) \cap \{k\}} 2^{n} = \sum_{n \in \{k\}} 2^{n}$
83		simplr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to k \in ℕ_{0}$
84	64	a1i	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to 2 \in ℕ$
85	84 83	nnexpcld	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to 2^{k} \in ℕ$
86	85	nncnd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to 2^{k} \in ℂ$
87		oveq2	$⊢ n = k \to 2^{n} = 2^{k}$
88	87	sumsn	$⊢ (k \in ℕ_{0} \land 2^{k} \in ℂ) \to \sum_{n \in \{k\}} 2^{n} = 2^{k}$
89	83 86 88	syl2anc	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to \sum_{n \in \{k\}} 2^{n} = 2^{k}$
90	82 89	eqtrd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land k \in bits (N)) \to \sum_{n \in bits (N) \cap \{k\}} 2^{n} = 2^{k}$
91		simpr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land \neg k \in bits (N)) \to \neg k \in bits (N)$
92		disjsn	$⊢ bits (N) \cap \{k\} = \emptyset \leftrightarrow \neg k \in bits (N)$
93	91 92	sylibr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land \neg k \in bits (N)) \to bits (N) \cap \{k\} = \emptyset$
94	93	sumeq1d	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land \neg k \in bits (N)) \to \sum_{n \in bits (N) \cap \{k\}} 2^{n} = \sum_{n \in \emptyset} 2^{n}$
95	94 8	eqtrdi	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land \neg k \in bits (N)) \to \sum_{n \in bits (N) \cap \{k\}} 2^{n} = 0$
96	76 77 90 95	ifbothda	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \sum_{n \in bits (N) \cap \{k\}} 2^{n} = if (k \in bits (N), 2^{k}, 0)$
97	96	oveq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (N \mod 2^{k}) + \sum_{n \in bits (N) \cap \{k\}} 2^{n} = (N \mod 2^{k}) + if (k \in bits (N), 2^{k}, 0)$
98	75 97	eqtr4d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \mod 2^{k + 1} = (N \mod 2^{k}) + \sum_{n \in bits (N) \cap \{k\}} 2^{n}$
99	73 98	eqeq12d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1} \leftrightarrow \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} + \sum_{n \in bits (N) \cap \{k\}} 2^{n} = (N \mod 2^{k}) + \sum_{n \in bits (N) \cap \{k\}} 2^{n})$
100	43 99	imbitrrid	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k} \to \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1})$
101	100	expcom	$⊢ k \in ℕ_{0} \to (N \in ℕ_{0} \to (\sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k} \to \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1}))$
102	101	a2d	$⊢ k \in ℕ_{0} \to ((N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^k)} 2^{n} = N \mod 2^{k}) \to (N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^k + 1)} 2^{n} = N \mod 2^{k + 1}))$
103	17 24 31 38 42 102	nn0ind	$⊢ N \in ℕ_{0} \to (N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n} = N \mod 2^{N})$
104	103	pm2.43i	$⊢ N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n} = N \mod 2^{N}$
105		id	$⊢ N \in ℕ_{0} \to N \in ℕ_{0}$
106	105 52	eleqtrdi	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq 0}$
107	64	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℕ$
108	107 105	nnexpcld	$⊢ N \in ℕ_{0} \to 2^{N} \in ℕ$
109	108	nnzd	$⊢ N \in ℕ_{0} \to 2^{N} \in ℤ$
110		2z	$⊢ 2 \in ℤ$
111		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
112	110 111	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
113		bernneq3	$⊢ (2 \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to N < 2^{N}$
114	112 113	mpan	$⊢ N \in ℕ_{0} \to N < 2^{N}$
115		elfzo2	$⊢ N \in (0 ..^2^{N}) \leftrightarrow (N \in ℤ_{\geq 0} \land 2^{N} \in ℤ \land N < 2^{N})$
116	106 109 114 115	syl3anbrc	$⊢ N \in ℕ_{0} \to N \in (0 ..^2^{N})$
117		bitsfzo	$⊢ (N \in ℤ \land N \in ℕ_{0}) \to (N \in (0 ..^2^{N}) \leftrightarrow bits (N) \subseteq (0 ..^N))$
118	39 105 117	syl2anc	$⊢ N \in ℕ_{0} \to (N \in (0 ..^2^{N}) \leftrightarrow bits (N) \subseteq (0 ..^N))$
119	116 118	mpbid	$⊢ N \in ℕ_{0} \to bits (N) \subseteq (0 ..^N)$
120		df-ss	$⊢ bits (N) \subseteq (0 ..^N) \leftrightarrow bits (N) \cap (0 ..^N) = bits (N)$
121	119 120	sylib	$⊢ N \in ℕ_{0} \to bits (N) \cap (0 ..^N) = bits (N)$
122	121	sumeq1d	$⊢ N \in ℕ_{0} \to \sum_{n \in bits (N) \cap (0 ..^N)} 2^{n} = \sum_{n \in bits (N)} 2^{n}$
123		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
124		2rp	$⊢ 2 \in ℝ^{+}$
125	124	a1i	$⊢ N \in ℕ_{0} \to 2 \in ℝ^{+}$
126	125 39	rpexpcld	$⊢ N \in ℕ_{0} \to 2^{N} \in ℝ^{+}$
127		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
128		modid	$⊢ ((N \in ℝ \land 2^{N} \in ℝ^{+}) \land (0 \leq N \land N < 2^{N})) \to N \mod 2^{N} = N$
129	123 126 127 114 128	syl22anc	$⊢ N \in ℕ_{0} \to N \mod 2^{N} = N$
130	104 122 129	3eqtr3d	$⊢ N \in ℕ_{0} \to \sum_{n \in bits (N)} 2^{n} = N$

Metamath Proof Explorer

Theorem bitsinv1

Proof