Theorem sadadd2

Description: Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-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}$$
Assertion	sadadd2	$$⊢\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)$$

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		oveq2	$$⊢x=0\to \left(0..^x\right)=\left(0..^0\right)$$
7		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
8	6 7	eqtrdi	$$⊢x=0\to \left(0..^x\right)=\varnothing$$
9	8	ineq2d	$$⊢x=0\to \left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)=\left(A\mathrm{sadd}B\right)\cap \varnothing$$
10		in0	$$⊢\left(A\mathrm{sadd}B\right)\cap \varnothing =\varnothing$$
11	9 10	eqtrdi	$$⊢x=0\to \left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)=\varnothing$$
12	11	fveq2d	$$⊢x=0\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)=K\left(\varnothing \right)$$
13		0nn0	$$⊢0\in {\mathbb{N}}_0$$
14		fvres	$$⊢0\in {\mathbb{N}}_0\to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)=\mathrm{bits}\left(0\right)$$
15	13 14	ax-mp	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)=\mathrm{bits}\left(0\right)$$
16		0bits	$$⊢\mathrm{bits}\left(0\right)=\varnothing$$
17	15 16	eqtr2i	$$⊢\varnothing =\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)$$
18	5 17	fveq12i	$$⊢K\left(\varnothing \right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\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		f1ocnvfv1	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge 0\in {\mathbb{N}}_0\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\right)=0$$
21	19 13 20	mp2an	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\right)=0$$
22	18 21	eqtri	$$⊢K\left(\varnothing \right)=0$$
23	12 22	eqtrdi	$$⊢x=0\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)=0$$
24		fveq2	$$⊢x=0\to C\left(x\right)=C\left(0\right)$$
25	24	eleq2d	$$⊢x=0\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(0\right)\right)$$
26		oveq2	$$⊢x=0\to 2^x=2^0$$
27	25 26	ifbieq1d	$$⊢x=0\to if\left(\varnothing \in C\left(x\right),2^x,0\right)=if\left(\varnothing \in C\left(0\right),2^0,0\right)$$
28	23 27	oveq12d	$$⊢x=0\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=0+if\left(\varnothing \in C\left(0\right),2^0,0\right)$$
29	8	ineq2d	$$⊢x=0\to A\cap \left(0..^x\right)=A\cap \varnothing$$
30		in0	$$⊢A\cap \varnothing =\varnothing$$
31	29 30	eqtrdi	$$⊢x=0\to A\cap \left(0..^x\right)=\varnothing$$
32	31	fveq2d	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)=K\left(\varnothing \right)$$
33	32 22	eqtrdi	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)=0$$
34	8	ineq2d	$$⊢x=0\to B\cap \left(0..^x\right)=B\cap \varnothing$$
35		in0	$$⊢B\cap \varnothing =\varnothing$$
36	34 35	eqtrdi	$$⊢x=0\to B\cap \left(0..^x\right)=\varnothing$$
37	36	fveq2d	$$⊢x=0\to K\left(B\cap \left(0..^x\right)\right)=K\left(\varnothing \right)$$
38	37 22	eqtrdi	$$⊢x=0\to K\left(B\cap \left(0..^x\right)\right)=0$$
39	33 38	oveq12d	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=0+0$$
40		00id	$$⊢0+0=0$$
41	39 40	eqtrdi	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=0$$
42	28 41	eqeq12d	$$⊢x=0\to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 0+if\left(\varnothing \in C\left(0\right),2^0,0\right)=0\right)$$
43	42	imbi2d	$$⊢x=0\to \left(\left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\phi \to 0+if\left(\varnothing \in C\left(0\right),2^0,0\right)=0\right)\right)$$
44		oveq2	$$⊢x=k\to \left(0..^x\right)=\left(0..^k\right)$$
45	44	ineq2d	$$⊢x=k\to \left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)$$
46	45	fveq2d	$$⊢x=k\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)$$
47		fveq2	$$⊢x=k\to C\left(x\right)=C\left(k\right)$$
48	47	eleq2d	$$⊢x=k\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(k\right)\right)$$
49		oveq2	$$⊢x=k\to 2^x=2^k$$
50	48 49	ifbieq1d	$$⊢x=k\to if\left(\varnothing \in C\left(x\right),2^x,0\right)=if\left(\varnothing \in C\left(k\right),2^k,0\right)$$
51	46 50	oveq12d	$$⊢x=k\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)$$
52	44	ineq2d	$$⊢x=k\to A\cap \left(0..^x\right)=A\cap \left(0..^k\right)$$
53	52	fveq2d	$$⊢x=k\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k\right)\right)$$
54	44	ineq2d	$$⊢x=k\to B\cap \left(0..^x\right)=B\cap \left(0..^k\right)$$
55	54	fveq2d	$$⊢x=k\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^k\right)\right)$$
56	53 55	oveq12d	$$⊢x=k\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)$$
57	51 56	eqeq12d	$$⊢x=k\to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)$$
58	57	imbi2d	$$⊢x=k\to \left(\left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)$$
59		oveq2	$$⊢x=k+1\to \left(0..^x\right)=\left(0..^k+1\right)$$
60	59	ineq2d	$$⊢x=k+1\to \left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)$$
61	60	fveq2d	$$⊢x=k+1\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)$$
62		fveq2	$$⊢x=k+1\to C\left(x\right)=C\left(k+1\right)$$
63	62	eleq2d	$$⊢x=k+1\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(k+1\right)\right)$$
64		oveq2	$$⊢x=k+1\to 2^x=2^{k+1}$$
65	63 64	ifbieq1d	$$⊢x=k+1\to if\left(\varnothing \in C\left(x\right),2^x,0\right)=if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)$$
66	61 65	oveq12d	$$⊢x=k+1\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)$$
67	59	ineq2d	$$⊢x=k+1\to A\cap \left(0..^x\right)=A\cap \left(0..^k+1\right)$$
68	67	fveq2d	$$⊢x=k+1\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k+1\right)\right)$$
69	59	ineq2d	$$⊢x=k+1\to B\cap \left(0..^x\right)=B\cap \left(0..^k+1\right)$$
70	69	fveq2d	$$⊢x=k+1\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^k+1\right)\right)$$
71	68 70	oveq12d	$$⊢x=k+1\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)$$
72	66 71	eqeq12d	$$⊢x=k+1\to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)$$
73	72	imbi2d	$$⊢x=k+1\to \left(\left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)$$
74		oveq2	$$⊢x=N\to \left(0..^x\right)=\left(0..^N\right)$$
75	74	ineq2d	$$⊢x=N\to \left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)$$
76	75	fveq2d	$$⊢x=N\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)=K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)$$
77		fveq2	$$⊢x=N\to C\left(x\right)=C\left(N\right)$$
78	77	eleq2d	$$⊢x=N\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(N\right)\right)$$
79		oveq2	$$⊢x=N\to 2^x=2^N$$
80	78 79	ifbieq1d	$$⊢x=N\to if\left(\varnothing \in C\left(x\right),2^x,0\right)=if\left(\varnothing \in C\left(N\right),2^N,0\right)$$
81	76 80	oveq12d	$$⊢x=N\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,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)$$
82	74	ineq2d	$$⊢x=N\to A\cap \left(0..^x\right)=A\cap \left(0..^N\right)$$
83	82	fveq2d	$$⊢x=N\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^N\right)\right)$$
84	74	ineq2d	$$⊢x=N\to B\cap \left(0..^x\right)=B\cap \left(0..^N\right)$$
85	84	fveq2d	$$⊢x=N\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^N\right)\right)$$
86	83 85	oveq12d	$$⊢x=N\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
87	81 86	eqeq12d	$$⊢x=N\to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 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)\right)$$
88	87	imbi2d	$$⊢x=N\to \left(\left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^x\right)\right)+if\left(\varnothing \in C\left(x\right),2^x,0\right)=K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\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)\right)\right)$$
89	1 2 3	sadc0	$$⊢\phi \to \neg \varnothing \in C\left(0\right)$$
90	89	iffalsed	$$⊢\phi \to if\left(\varnothing \in C\left(0\right),2^0,0\right)=0$$
91	90	oveq2d	$$⊢\phi \to 0+if\left(\varnothing \in C\left(0\right),2^0,0\right)=0+0$$
92	91 40	eqtrdi	$$⊢\phi \to 0+if\left(\varnothing \in C\left(0\right),2^0,0\right)=0$$
93	1	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to A\subseteq {\mathbb{N}}_0$$
94	2	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to B\subseteq {\mathbb{N}}_0$$
95		simplr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to k\in {\mathbb{N}}_0$$
96		simpr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)$$
97	93 94 3 95 5 96	sadadd2lem	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)$$
98	97	ex	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)$$
99	98	expcom	$$⊢k\in {\mathbb{N}}_0\to \left(\phi \to \left(K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)$$
100	99	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k\right)\right)+if\left(\varnothing \in C\left(k\right),2^k,0\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to \left(\phi \to K\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^k+1\right)\right)+if\left(\varnothing \in C\left(k+1\right),2^{k+1},0\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)$$
101	43 58 73 88 92 100	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\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)\right)$$
102	4 101	mpcom	$$⊢\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)$$