bitsinvp1

Description: Recursive definition of the inverse of the bits function. (Contributed by Mario Carneiro, 8-Sep-2016)

		Ref	Expression
	Hypothesis	bitsinv.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
	Assertion	bitsinvp1	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to K (A \cap (0 ..^N + 1)) = K (A \cap (0 ..^N)) + if (N \in A, 2^{N}, 0)$

Proof

Step	Hyp	Ref	Expression
1		bitsinv.k	$⊢ K = {({bits ↾}_{ℕ_{0}})}^{-1}$
2		fzonel	$⊢ \neg N \in (0 ..^N)$
3	2	a1i	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to \neg N \in (0 ..^N)$
4		disjsn	$⊢ (0 ..^N) \cap \{N\} = \emptyset \leftrightarrow \neg N \in (0 ..^N)$
5	3 4	sylibr	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to (0 ..^N) \cap \{N\} = \emptyset$
6	5	ineq2d	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap ((0 ..^N) \cap \{N\}) = A \cap \emptyset$
7		inindi	$⊢ A \cap ((0 ..^N) \cap \{N\}) = (A \cap (0 ..^N)) \cap (A \cap \{N\})$
8		in0	$⊢ A \cap \emptyset = \emptyset$
9	6 7 8	3eqtr3g	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to (A \cap (0 ..^N)) \cap (A \cap \{N\}) = \emptyset$
10		simpr	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to N \in ℕ_{0}$
11		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
12	10 11	eleqtrdi	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
13		fzosplitsn	$⊢ N \in ℤ_{\geq 0} \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
14	12 13	syl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to (0 ..^N + 1) = (0 ..^N) \cup \{N\}$
15	14	ineq2d	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N + 1) = A \cap ((0 ..^N) \cup \{N\})$
16		indi	$⊢ A \cap ((0 ..^N) \cup \{N\}) = (A \cap (0 ..^N)) \cup (A \cap \{N\})$
17	15 16	eqtrdi	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N + 1) = (A \cap (0 ..^N)) \cup (A \cap \{N\})$
18		fzofi	$⊢ (0 ..^N + 1) \in Fin$
19	18	a1i	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to (0 ..^N + 1) \in Fin$
20		inss2	$⊢ A \cap (0 ..^N + 1) \subseteq (0 ..^N + 1)$
21		ssfi	$⊢ ((0 ..^N + 1) \in Fin \land A \cap (0 ..^N + 1) \subseteq (0 ..^N + 1)) \to A \cap (0 ..^N + 1) \in Fin$
22	19 20 21	sylancl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N + 1) \in Fin$
23		2nn	$⊢ 2 \in ℕ$
24	23	a1i	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land k \in (A \cap (0 ..^N + 1))) \to 2 \in ℕ$
25		inss1	$⊢ A \cap (0 ..^N + 1) \subseteq A$
26		simpl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \subseteq ℕ_{0}$
27	25 26	sstrid	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N + 1) \subseteq ℕ_{0}$
28	27	sselda	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land k \in (A \cap (0 ..^N + 1))) \to k \in ℕ_{0}$
29	24 28	nnexpcld	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land k \in (A \cap (0 ..^N + 1))) \to 2^{k} \in ℕ$
30	29	nncnd	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land k \in (A \cap (0 ..^N + 1))) \to 2^{k} \in ℂ$
31	9 17 22 30	fsumsplit	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to \sum_{k \in A \cap (0 ..^N + 1)} 2^{k} = \sum_{k \in A \cap (0 ..^N)} 2^{k} + \sum_{k \in A \cap \{N\}} 2^{k}$
32		elfpw	$⊢ A \cap (0 ..^N + 1) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (A \cap (0 ..^N + 1) \subseteq ℕ_{0} \land A \cap (0 ..^N + 1) \in Fin)$
33	27 22 32	sylanbrc	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N + 1) \in (𝒫 ℕ_{0} \cap Fin)$
34	1	bitsinv	$⊢ A \cap (0 ..^N + 1) \in (𝒫 ℕ_{0} \cap Fin) \to K (A \cap (0 ..^N + 1)) = \sum_{k \in A \cap (0 ..^N + 1)} 2^{k}$
35	33 34	syl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to K (A \cap (0 ..^N + 1)) = \sum_{k \in A \cap (0 ..^N + 1)} 2^{k}$
36		inss1	$⊢ A \cap (0 ..^N) \subseteq A$
37	36 26	sstrid	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N) \subseteq ℕ_{0}$
38		fzofi	$⊢ (0 ..^N) \in Fin$
39	38	a1i	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to (0 ..^N) \in Fin$
40		inss2	$⊢ A \cap (0 ..^N) \subseteq (0 ..^N)$
41		ssfi	$⊢ ((0 ..^N) \in Fin \land A \cap (0 ..^N) \subseteq (0 ..^N)) \to A \cap (0 ..^N) \in Fin$
42	39 40 41	sylancl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N) \in Fin$
43		elfpw	$⊢ A \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \leftrightarrow (A \cap (0 ..^N) \subseteq ℕ_{0} \land A \cap (0 ..^N) \in Fin)$
44	37 42 43	sylanbrc	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to A \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin)$
45	1	bitsinv	$⊢ A \cap (0 ..^N) \in (𝒫 ℕ_{0} \cap Fin) \to K (A \cap (0 ..^N)) = \sum_{k \in A \cap (0 ..^N)} 2^{k}$
46	44 45	syl	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to K (A \cap (0 ..^N)) = \sum_{k \in A \cap (0 ..^N)} 2^{k}$
47		snssi	$⊢ N \in A \to \{N\} \subseteq A$
48	47	adantl	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to \{N\} \subseteq A$
49		sseqin2	$⊢ \{N\} \subseteq A \leftrightarrow A \cap \{N\} = \{N\}$
50	48 49	sylib	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to A \cap \{N\} = \{N\}$
51	50	sumeq1d	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to \sum_{k \in A \cap \{N\}} 2^{k} = \sum_{k \in \{N\}} 2^{k}$
52		simpr	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to N \in A$
53	23	a1i	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to 2 \in ℕ$
54		simplr	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to N \in ℕ_{0}$
55	53 54	nnexpcld	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to 2^{N} \in ℕ$
56	55	nncnd	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to 2^{N} \in ℂ$
57		oveq2	$⊢ k = N \to 2^{k} = 2^{N}$
58	57	sumsn	$⊢ (N \in A \land 2^{N} \in ℂ) \to \sum_{k \in \{N\}} 2^{k} = 2^{N}$
59	52 56 58	syl2anc	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to \sum_{k \in \{N\}} 2^{k} = 2^{N}$
60	51 59	eqtr2d	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land N \in A) \to 2^{N} = \sum_{k \in A \cap \{N\}} 2^{k}$
61		simpr	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land \neg N \in A) \to \neg N \in A$
62		disjsn	$⊢ A \cap \{N\} = \emptyset \leftrightarrow \neg N \in A$
63	61 62	sylibr	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land \neg N \in A) \to A \cap \{N\} = \emptyset$
64	63	sumeq1d	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land \neg N \in A) \to \sum_{k \in A \cap \{N\}} 2^{k} = \sum_{k \in \emptyset} 2^{k}$
65		sum0	$⊢ \sum_{k \in \emptyset} 2^{k} = 0$
66	64 65	eqtr2di	$⊢ ((A \subseteq ℕ_{0} \land N \in ℕ_{0}) \land \neg N \in A) \to 0 = \sum_{k \in A \cap \{N\}} 2^{k}$
67	60 66	ifeqda	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to if (N \in A, 2^{N}, 0) = \sum_{k \in A \cap \{N\}} 2^{k}$
68	46 67	oveq12d	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to K (A \cap (0 ..^N)) + if (N \in A, 2^{N}, 0) = \sum_{k \in A \cap (0 ..^N)} 2^{k} + \sum_{k \in A \cap \{N\}} 2^{k}$
69	31 35 68	3eqtr4d	$⊢ (A \subseteq ℕ_{0} \land N \in ℕ_{0}) \to K (A \cap (0 ..^N + 1)) = K (A \cap (0 ..^N)) + if (N \in A, 2^{N}, 0)$

Metamath Proof Explorer

Theorem bitsinvp1

Proof