Theorem sadadd2lem

Description: Lemma for sadadd2 . (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
	sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sadcadd.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
	sadadd2lem.1	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
Assertion	sadadd2lem	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N+1\right)\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		sadcadd.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
6		sadadd2lem.1	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
7		inss1	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq A\mathrm{sadd}B$$
8	1 2 3	sadfval	$$⊢\phi \to A\mathrm{sadd}B=\left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}$$
9		ssrab2	$$⊢\left\{k\in {\mathbb{N}}_0|hadd\left(k\in A,k\in B,\varnothing \in C\left(k\right)\right)\right\}\subseteq {\mathbb{N}}_0$$
10	8 9	eqsstrdi	$$⊢\phi \to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
11	7 10	sstrid	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
12		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
13	12	a1i	$$⊢\phi \to \left(0..^N\right)\in \mathrm{Fin}$$
14		inss2	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
15		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
16	13 14 15	sylancl	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
17		elfpw	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
18	11 16 17	sylanbrc	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
19		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
20		f1ocnv	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
21		f1of	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
22	19 20 21	mp2b	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
23	5	feq1i	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0\leftrightarrow {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
24	22 23	mpbir	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
25	24	ffvelrni	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
26	18 25	syl	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
27	26	nn0cnd	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in ℂ$$
28		2nn0	$$⊢2\in {\mathbb{N}}_0$$
29	28	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
30	29 4	nn0expcld	$$⊢\phi \to 2^N\in {\mathbb{N}}_0$$
31		0nn0	$$⊢0\in {\mathbb{N}}_0$$
32		ifcl	$$⊢\left(2^N\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)\in {\mathbb{N}}_0$$
33	30 31 32	sylancl	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)\in {\mathbb{N}}_0$$
34	33	nn0cnd	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)\in ℂ$$
35		1nn0	$$⊢1\in {\mathbb{N}}_0$$
36	35	a1i	$$⊢\phi \to 1\in {\mathbb{N}}_0$$
37	4 36	nn0addcld	$$⊢\phi \to N+1\in {\mathbb{N}}_0$$
38	29 37	nn0expcld	$$⊢\phi \to 2^{N+1}\in {\mathbb{N}}_0$$
39		ifcl	$$⊢\left(2^{N+1}\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\in {\mathbb{N}}_0$$
40	38 31 39	sylancl	$$⊢\phi \to if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\in {\mathbb{N}}_0$$
41	40	nn0cnd	$$⊢\phi \to if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\in ℂ$$
42	34 41	addcld	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\in ℂ$$
43	27 42	addcld	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\in ℂ$$
44		inss1	$$⊢A\cap \left(0..^N\right)\subseteq A$$
45	44 1	sstrid	$$⊢\phi \to A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
46		inss2	$$⊢A\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
47		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge A\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to A\cap \left(0..^N\right)\in \mathrm{Fin}$$
48	13 46 47	sylancl	$$⊢\phi \to A\cap \left(0..^N\right)\in \mathrm{Fin}$$
49		elfpw	$$⊢A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge A\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
50	45 48 49	sylanbrc	$$⊢\phi \to A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
51	24	ffvelrni	$$⊢A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to K\left(A\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
52	50 51	syl	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
53	52	nn0cnd	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in ℂ$$
54		inss1	$$⊢B\cap \left(0..^N\right)\subseteq B$$
55	54 2	sstrid	$$⊢\phi \to B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
56		inss2	$$⊢B\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
57		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge B\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to B\cap \left(0..^N\right)\in \mathrm{Fin}$$
58	13 56 57	sylancl	$$⊢\phi \to B\cap \left(0..^N\right)\in \mathrm{Fin}$$
59		elfpw	$$⊢B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge B\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
60	55 58 59	sylanbrc	$$⊢\phi \to B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
61	24	ffvelrni	$$⊢B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to K\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
62	60 61	syl	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
63	62	nn0cnd	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in ℂ$$
64	53 63	addcld	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℂ$$
65		ifcl	$$⊢\left(2^N\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(N\in A,2^N,0\right)\in {\mathbb{N}}_0$$
66	30 31 65	sylancl	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in {\mathbb{N}}_0$$
67	66	nn0cnd	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in ℂ$$
68		ifcl	$$⊢\left(2^N\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to if\left(N\in B,2^N,0\right)\in {\mathbb{N}}_0$$
69	30 31 68	sylancl	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in {\mathbb{N}}_0$$
70	69	nn0cnd	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in ℂ$$
71	67 70	addcld	$$⊢\phi \to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℂ$$
72	64 71	addcld	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℂ$$
73	30	nn0cnd	$$⊢\phi \to 2^N\in ℂ$$
74	73	adantr	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to 2^N\in ℂ$$
75		0cnd	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to 0\in ℂ$$
76	74 75	ifclda	$$⊢\phi \to if\left(\varnothing \in C\left(N\right),2^N,0\right)\in ℂ$$
77	1 2 3 4	sadval	$$⊢\phi \to \left(N\in \left(A\mathrm{sadd}B\right)\leftrightarrow hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$
78	77	ifbid	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)=if\left(hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),2^N,0\right)$$
79	1 2 3 4	sadcp1	$$⊢\phi \to \left(\varnothing \in C\left(N+1\right)\leftrightarrow cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\right)$$
80	29	nn0cnd	$$⊢\phi \to 2\in ℂ$$
81	80 4	expp1d	$$⊢\phi \to 2^{N+1}=2^N\cdot 2$$
82	73 80	mulcomd	$$⊢\phi \to 2^N\cdot 2=22^N$$
83	81 82	eqtrd	$$⊢\phi \to 2^{N+1}=22^N$$
84	79 83	ifbieq1d	$$⊢\phi \to if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=if\left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),22^N,0\right)$$
85	78 84	oveq12d	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=if\left(hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),2^N,0\right)+if\left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),22^N,0\right)$$
86		sadadd2lem2	$$⊢2^N\in ℂ\to if\left(hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),2^N,0\right)+if\left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),22^N,0\right)=if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
87	73 86	syl	$$⊢\phi \to if\left(hadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),2^N,0\right)+if\left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right),22^N,0\right)=if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
88	85 87	eqtrd	$$⊢\phi \to if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
89	6 88	oveq12d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+\left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
90	27 42 76	add32d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+\left(if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)$$
91	64 71 76	addassd	$$⊢\phi \to \left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)+\left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+\left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
92	89 90 91	3eqtr4d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+\left(if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)=\left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)+\left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\right)+if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
93	43 72 76 92	addcan2ad	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)$$
94	27 34 41	addassd	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)$$
95	53 67 63 70	add4d	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in B,2^N,0\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)$$
96	93 94 95	3eqtr4d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(A\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in B,2^N,0\right)$$
97	5	bitsinvp1	$$⊢\left(A\mathrm{sadd}B\subseteq {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N+1\right)\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)$$
98	10 4 97	syl2anc	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N+1\right)\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)$$
99	98	oveq1d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N+1\right)\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+if\left(N\in \left(A\mathrm{sadd}B\right),2^N,0\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)$$
100	5	bitsinvp1	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to K\left(A\cap \left(0..^N+1\right)\right)=K\left(A\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)$$
101	1 4 100	syl2anc	$$⊢\phi \to K\left(A\cap \left(0..^N+1\right)\right)=K\left(A\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)$$
102	5	bitsinvp1	$$⊢\left(B\subseteq {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to K\left(B\cap \left(0..^N+1\right)\right)=K\left(B\cap \left(0..^N\right)\right)+if\left(N\in B,2^N,0\right)$$
103	2 4 102	syl2anc	$$⊢\phi \to K\left(B\cap \left(0..^N+1\right)\right)=K\left(B\cap \left(0..^N\right)\right)+if\left(N\in B,2^N,0\right)$$
104	101 103	oveq12d	$$⊢\phi \to K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\right)=K\left(A\cap \left(0..^N\right)\right)+if\left(N\in A,2^N,0\right)+K\left(B\cap \left(0..^N\right)\right)+if\left(N\in B,2^N,0\right)$$
105	96 99 104	3eqtr4d	$$⊢\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N+1\right)\right)+if\left(\varnothing \in C\left(N+1\right),2^{N+1},0\right)=K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\right)$$