Theorem sadcaddlem

Description: Lemma for sadcadd . (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}$$
	sadcaddlem.1	$$⊢\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)$$
Assertion	sadcaddlem	$$⊢\phi \to \left(\varnothing \in C\left(N+1\right)\leftrightarrow 2^{N+1}\le K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\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		sadcaddlem.1	$$⊢\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)$$
7		cad1	$$⊢\varnothing \in C\left(N\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow \left(N\in A\vee N\in B\right)\right)$$
8	7	adantl	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow \left(N\in A\vee N\in B\right)\right)$$
9		2nn	$$⊢2\in \mathbb{N}$$
10	9	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
11	10 4	nnexpcld	$$⊢\phi \to 2^N\in \mathbb{N}$$
12	11	nnred	$$⊢\phi \to 2^N\in ℝ$$
13	12	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to 2^N\in ℝ$$
14		inss1	$$⊢A\cap \left(0..^N\right)\subseteq A$$
15	14 1	sstrid	$$⊢\phi \to A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
16		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
17	16	a1i	$$⊢\phi \to \left(0..^N\right)\in \mathrm{Fin}$$
18		inss2	$$⊢A\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
19		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}$$
20	17 18 19	sylancl	$$⊢\phi \to A\cap \left(0..^N\right)\in \mathrm{Fin}$$
21		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)$$
22	15 20 21	sylanbrc	$$⊢\phi \to A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
23		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
24		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$$
25	23 24	ax-mp	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
26		f1oeq1	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\to \left(K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\right)$$
27	5 26	ax-mp	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
28	25 27	mpbir	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
29		f1of	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
30	28 29	ax-mp	$$⊢K:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
31	30	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$$
32	22 31	syl	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
33		inss1	$$⊢B\cap \left(0..^N\right)\subseteq B$$
34	33 2	sstrid	$$⊢\phi \to B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
35		inss2	$$⊢B\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
36		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}$$
37	17 35 36	sylancl	$$⊢\phi \to B\cap \left(0..^N\right)\in \mathrm{Fin}$$
38		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)$$
39	34 37 38	sylanbrc	$$⊢\phi \to B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
40	30	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$$
41	39 40	syl	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
42	32 41	nn0addcld	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
43	42	nn0red	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
44	43	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
45		2nn0	$$⊢2\in {\mathbb{N}}_0$$
46	45	a1i	$$⊢\left(\phi \wedge N\in A\right)\to 2\in {\mathbb{N}}_0$$
47	4	adantr	$$⊢\left(\phi \wedge N\in A\right)\to N\in {\mathbb{N}}_0$$
48	46 47	nn0expcld	$$⊢\left(\phi \wedge N\in A\right)\to 2^N\in {\mathbb{N}}_0$$
49		0nn0	$$⊢0\in {\mathbb{N}}_0$$
50	49	a1i	$$⊢\left(\phi \wedge \neg N\in A\right)\to 0\in {\mathbb{N}}_0$$
51	48 50	ifclda	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in {\mathbb{N}}_0$$
52	45	a1i	$$⊢\left(\phi \wedge N\in B\right)\to 2\in {\mathbb{N}}_0$$
53	4	adantr	$$⊢\left(\phi \wedge N\in B\right)\to N\in {\mathbb{N}}_0$$
54	52 53	nn0expcld	$$⊢\left(\phi \wedge N\in B\right)\to 2^N\in {\mathbb{N}}_0$$
55	49	a1i	$$⊢\left(\phi \wedge \neg N\in B\right)\to 0\in {\mathbb{N}}_0$$
56	54 55	ifclda	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in {\mathbb{N}}_0$$
57	51 56	nn0addcld	$$⊢\phi \to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in {\mathbb{N}}_0$$
58	57	nn0red	$$⊢\phi \to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℝ$$
59	58	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℝ$$
60	6	biimpa	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
61	60	adantr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
62	11	nnnn0d	$$⊢\phi \to 2^N\in {\mathbb{N}}_0$$
63		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$$
64	62 49 63	sylancl	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in {\mathbb{N}}_0$$
65	64	nn0ge0d	$$⊢\phi \to 0\le if\left(N\in B,2^N,0\right)$$
66	12	adantr	$$⊢\left(\phi \wedge N\in B\right)\to 2^N\in ℝ$$
67		0red	$$⊢\left(\phi \wedge \neg N\in B\right)\to 0\in ℝ$$
68	66 67	ifclda	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in ℝ$$
69	12 68	addge01d	$$⊢\phi \to \left(0\le if\left(N\in B,2^N,0\right)\leftrightarrow 2^N\le 2^N+if\left(N\in B,2^N,0\right)\right)$$
70	65 69	mpbid	$$⊢\phi \to 2^N\le 2^N+if\left(N\in B,2^N,0\right)$$
71	70	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in A\right)\to 2^N\le 2^N+if\left(N\in B,2^N,0\right)$$
72		iftrue	$$⊢N\in A\to if\left(N\in A,2^N,0\right)=2^N$$
73	72	adantl	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in A\right)\to if\left(N\in A,2^N,0\right)=2^N$$
74	73	oveq1d	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in A\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=2^N+if\left(N\in B,2^N,0\right)$$
75	71 74	breqtrrd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in A\right)\to 2^N\le if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)$$
76		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$$
77	62 49 76	sylancl	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in {\mathbb{N}}_0$$
78	77	nn0ge0d	$$⊢\phi \to 0\le if\left(N\in A,2^N,0\right)$$
79	12	adantr	$$⊢\left(\phi \wedge N\in A\right)\to 2^N\in ℝ$$
80		0red	$$⊢\left(\phi \wedge \neg N\in A\right)\to 0\in ℝ$$
81	79 80	ifclda	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in ℝ$$
82	12 81	addge02d	$$⊢\phi \to \left(0\le if\left(N\in A,2^N,0\right)\leftrightarrow 2^N\le if\left(N\in A,2^N,0\right)+2^N\right)$$
83	78 82	mpbid	$$⊢\phi \to 2^N\le if\left(N\in A,2^N,0\right)+2^N$$
84	83	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in B\right)\to 2^N\le if\left(N\in A,2^N,0\right)+2^N$$
85		iftrue	$$⊢N\in B\to if\left(N\in B,2^N,0\right)=2^N$$
86	85	adantl	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in B\right)\to if\left(N\in B,2^N,0\right)=2^N$$
87	86	oveq2d	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in B\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=if\left(N\in A,2^N,0\right)+2^N$$
88	84 87	breqtrrd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge N\in B\right)\to 2^N\le if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)$$
89	75 88	jaodan	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to 2^N\le if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)$$
90	13 13 44 59 61 89	le2addd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\vee N\in B\right)\right)\to 2^N+2^N\le 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)$$
91	90	ex	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(\left(N\in A\vee N\in B\right)\to 2^N+2^N\le 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)\right)$$
92		ioran	$$⊢\neg \left(N\in A\vee N\in B\right)\leftrightarrow \left(\neg N\in A\wedge \neg N\in B\right)$$
93		iffalse	$$⊢\neg N\in A\to if\left(N\in A,2^N,0\right)=0$$
94	93	ad2antrl	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in A,2^N,0\right)=0$$
95		iffalse	$$⊢\neg N\in B\to if\left(N\in B,2^N,0\right)=0$$
96	95	ad2antll	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in B,2^N,0\right)=0$$
97	94 96	oveq12d	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=0+0$$
98		00id	$$⊢0+0=0$$
99	97 98	syl6eq	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=0$$
100	99	oveq2d	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\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)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+0$$
101	32	nn0red	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in ℝ$$
102	101	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)\in ℝ$$
103	41	nn0red	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
104	103	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
105	102 104	readdcld	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
106	105	recnd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℂ$$
107	106	addid1d	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+0=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
108	100 107	eqtrd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\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)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
109	5	fveq1i	$$⊢K\left(A\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)$$
110	109	fveq2i	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(K\left(A\cap \left(0..^N\right)\right)\right)=\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\right)$$
111	32	fvresd	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(K\left(A\cap \left(0..^N\right)\right)\right)=\mathrm{bits}\left(K\left(A\cap \left(0..^N\right)\right)\right)$$
112		f1ocnvfv2	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\right)=A\cap \left(0..^N\right)$$
113	23 22 112	sylancr	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\right)=A\cap \left(0..^N\right)$$
114	110 111 113	3eqtr3a	$$⊢\phi \to \mathrm{bits}\left(K\left(A\cap \left(0..^N\right)\right)\right)=A\cap \left(0..^N\right)$$
115	114 18	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left(K\left(A\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
116	32	nn0zd	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in \mathbb{Z}$$
117		bitsfzo	$$⊢\left(K\left(A\cap \left(0..^N\right)\right)\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left(K\left(A\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left(K\left(A\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
118	116 4 117	syl2anc	$$⊢\phi \to \left(K\left(A\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left(K\left(A\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
119	115 118	mpbird	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)$$
120		elfzolt2	$$⊢K\left(A\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\to K\left(A\cap \left(0..^N\right)\right)<2^N$$
121	119 120	syl	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)<2^N$$
122	5	fveq1i	$$⊢K\left(B\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)$$
123	122	fveq2i	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(K\left(B\cap \left(0..^N\right)\right)\right)=\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\right)$$
124	41	fvresd	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(K\left(B\cap \left(0..^N\right)\right)\right)=\mathrm{bits}\left(K\left(B\cap \left(0..^N\right)\right)\right)$$
125		f1ocnvfv2	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\right)=B\cap \left(0..^N\right)$$
126	23 39 125	sylancr	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\right)=B\cap \left(0..^N\right)$$
127	123 124 126	3eqtr3a	$$⊢\phi \to \mathrm{bits}\left(K\left(B\cap \left(0..^N\right)\right)\right)=B\cap \left(0..^N\right)$$
128	127 35	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left(K\left(B\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
129	41	nn0zd	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in \mathbb{Z}$$
130		bitsfzo	$$⊢\left(K\left(B\cap \left(0..^N\right)\right)\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left(K\left(B\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left(K\left(B\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
131	129 4 130	syl2anc	$$⊢\phi \to \left(K\left(B\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left(K\left(B\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
132	128 131	mpbird	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)$$
133		elfzolt2	$$⊢K\left(B\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\to K\left(B\cap \left(0..^N\right)\right)<2^N$$
134	132 133	syl	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)<2^N$$
135	101 103 12 12 121 134	lt2addd	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N+2^N$$
136	135	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N+2^N$$
137	108 136	eqbrtrd	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\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)<2^N+2^N$$
138	81	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in A,2^N,0\right)\in ℝ$$
139	68	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in B,2^N,0\right)\in ℝ$$
140	138 139	readdcld	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℝ$$
141	105 140	readdcld	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\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 ℝ$$
142	12	ad2antrr	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to 2^N\in ℝ$$
143	142 142	readdcld	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to 2^N+2^N\in ℝ$$
144	141 143	ltnled	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to \left(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)<2^N+2^N\leftrightarrow \neg 2^N+2^N\le 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)\right)$$
145	137 144	mpbid	$$⊢\left(\left(\phi \wedge \varnothing \in C\left(N\right)\right)\wedge \left(\neg N\in A\wedge \neg N\in B\right)\right)\to \neg 2^N+2^N\le 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)$$
146	145	ex	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(\left(\neg N\in A\wedge \neg N\in B\right)\to \neg 2^N+2^N\le 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)\right)$$
147	92 146	syl5bi	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(\neg \left(N\in A\vee N\in B\right)\to \neg 2^N+2^N\le 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)\right)$$
148	91 147	impcon4bid	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(\left(N\in A\vee N\in B\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
149	8 148	bitrd	$$⊢\left(\phi \wedge \varnothing \in C\left(N\right)\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
150		cad0	$$⊢\neg \varnothing \in C\left(N\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow \left(N\in A\wedge N\in B\right)\right)$$
151	150	adantl	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow \left(N\in A\wedge N\in B\right)\right)$$
152	42	nn0ge0d	$$⊢\phi \to 0\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
153	12 12	readdcld	$$⊢\phi \to 2^N+2^N\in ℝ$$
154	153 43	addge02d	$$⊢\phi \to \left(0\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\leftrightarrow 2^N+2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N+2^N\right)$$
155	152 154	mpbid	$$⊢\phi \to 2^N+2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N+2^N$$
156	155	ad2antrr	$$⊢\left(\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\wedge N\in B\right)\right)\to 2^N+2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N+2^N$$
157	72 85	oveqan12d	$$⊢\left(N\in A\wedge N\in B\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=2^N+2^N$$
158	157	adantl	$$⊢\left(\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\wedge N\in B\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=2^N+2^N$$
159	158	oveq2d	$$⊢\left(\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\wedge N\in B\right)\right)\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)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N+2^N$$
160	156 159	breqtrrd	$$⊢\left(\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\wedge \left(N\in A\wedge N\in B\right)\right)\to 2^N+2^N\le 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)$$
161	160	ex	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(\left(N\in A\wedge N\in B\right)\to 2^N+2^N\le 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)\right)$$
162	101	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)\in ℝ$$
163	103	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
164	162 163	readdcld	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
165	12	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to 2^N\in ℝ$$
166	12 43	lenltd	$$⊢\phi \to \left(2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\leftrightarrow \neg K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N\right)$$
167	6 166	bitrd	$$⊢\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow \neg K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N\right)$$
168	167	con2bid	$$⊢\phi \to \left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N\leftrightarrow \neg \varnothing \in C\left(N\right)\right)$$
169	168	biimpar	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)<2^N$$
170	164 165 165 169	ltadd1dd	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<2^N+2^N$$
171	164 165	readdcld	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N\in ℝ$$
172	153	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to 2^N+2^N\in ℝ$$
173	43 58	readdcld	$$⊢\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 ℝ$$
174	173	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\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 ℝ$$
175		ltletr	$$⊢\left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N\in ℝ\wedge 2^N+2^N\in ℝ\wedge 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 ℝ\right)\to \left(\left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<2^N+2^N\wedge 2^N+2^N\le 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)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<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)\right)$$
176	171 172 174 175	syl3anc	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(\left(K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<2^N+2^N\wedge 2^N+2^N\le 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)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<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)\right)$$
177	170 176	mpand	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(2^N+2^N\le 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)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<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)\right)$$
178	58	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\in ℝ$$
179	43	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\in ℝ$$
180	165 178 179	ltadd2d	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(2^N<if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\leftrightarrow K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)+2^N<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)\right)$$
181	177 180	sylibrd	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(2^N+2^N\le 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)\to 2^N<if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\right)$$
182	12 58	ltnled	$$⊢\phi \to \left(2^N<if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\leftrightarrow \neg if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\right)$$
183	64	nn0cnd	$$⊢\phi \to if\left(N\in B,2^N,0\right)\in ℂ$$
184	183	addid2d	$$⊢\phi \to 0+if\left(N\in B,2^N,0\right)=if\left(N\in B,2^N,0\right)$$
185	12	leidd	$$⊢\phi \to 2^N\le 2^N$$
186	62	nn0ge0d	$$⊢\phi \to 0\le 2^N$$
187		breq1	$$⊢2^N=if\left(N\in B,2^N,0\right)\to \left(2^N\le 2^N\leftrightarrow if\left(N\in B,2^N,0\right)\le 2^N\right)$$
188		breq1	$$⊢0=if\left(N\in B,2^N,0\right)\to \left(0\le 2^N\leftrightarrow if\left(N\in B,2^N,0\right)\le 2^N\right)$$
189	187 188	ifboth	$$⊢\left(2^N\le 2^N\wedge 0\le 2^N\right)\to if\left(N\in B,2^N,0\right)\le 2^N$$
190	185 186 189	syl2anc	$$⊢\phi \to if\left(N\in B,2^N,0\right)\le 2^N$$
191	184 190	eqbrtrd	$$⊢\phi \to 0+if\left(N\in B,2^N,0\right)\le 2^N$$
192	93	oveq1d	$$⊢\neg N\in A\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=0+if\left(N\in B,2^N,0\right)$$
193	192	breq1d	$$⊢\neg N\in A\to \left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\leftrightarrow 0+if\left(N\in B,2^N,0\right)\le 2^N\right)$$
194	191 193	syl5ibrcom	$$⊢\phi \to \left(\neg N\in A\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\right)$$
195	194	con1d	$$⊢\phi \to \left(\neg if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\to N\in A\right)$$
196	77	nn0cnd	$$⊢\phi \to if\left(N\in A,2^N,0\right)\in ℂ$$
197	196	addid1d	$$⊢\phi \to if\left(N\in A,2^N,0\right)+0=if\left(N\in A,2^N,0\right)$$
198		breq1	$$⊢2^N=if\left(N\in A,2^N,0\right)\to \left(2^N\le 2^N\leftrightarrow if\left(N\in A,2^N,0\right)\le 2^N\right)$$
199		breq1	$$⊢0=if\left(N\in A,2^N,0\right)\to \left(0\le 2^N\leftrightarrow if\left(N\in A,2^N,0\right)\le 2^N\right)$$
200	198 199	ifboth	$$⊢\left(2^N\le 2^N\wedge 0\le 2^N\right)\to if\left(N\in A,2^N,0\right)\le 2^N$$
201	185 186 200	syl2anc	$$⊢\phi \to if\left(N\in A,2^N,0\right)\le 2^N$$
202	197 201	eqbrtrd	$$⊢\phi \to if\left(N\in A,2^N,0\right)+0\le 2^N$$
203	95	oveq2d	$$⊢\neg N\in B\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)=if\left(N\in A,2^N,0\right)+0$$
204	203	breq1d	$$⊢\neg N\in B\to \left(if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\leftrightarrow if\left(N\in A,2^N,0\right)+0\le 2^N\right)$$
205	202 204	syl5ibrcom	$$⊢\phi \to \left(\neg N\in B\to if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\right)$$
206	205	con1d	$$⊢\phi \to \left(\neg if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\to N\in B\right)$$
207	195 206	jcad	$$⊢\phi \to \left(\neg if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\le 2^N\to \left(N\in A\wedge N\in B\right)\right)$$
208	182 207	sylbid	$$⊢\phi \to \left(2^N<if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\to \left(N\in A\wedge N\in B\right)\right)$$
209	208	adantr	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(2^N<if\left(N\in A,2^N,0\right)+if\left(N\in B,2^N,0\right)\to \left(N\in A\wedge N\in B\right)\right)$$
210	181 209	syld	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(2^N+2^N\le 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)\to \left(N\in A\wedge N\in B\right)\right)$$
211	161 210	impbid	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(\left(N\in A\wedge N\in B\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
212	151 211	bitrd	$$⊢\left(\phi \wedge \neg \varnothing \in C\left(N\right)\right)\to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
213	149 212	pm2.61dan	$$⊢\phi \to \left(cadd\left(N\in A,N\in B,\varnothing \in C\left(N\right)\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
214	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)$$
215		2cnd	$$⊢\phi \to 2\in ℂ$$
216	215 4	expp1d	$$⊢\phi \to 2^{N+1}=2^N\cdot 2$$
217	11	nncnd	$$⊢\phi \to 2^N\in ℂ$$
218	217	times2d	$$⊢\phi \to 2^N\cdot 2=2^N+2^N$$
219	216 218	eqtrd	$$⊢\phi \to 2^{N+1}=2^N+2^N$$
220	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)$$
221	1 4 220	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)$$
222	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)$$
223	2 4 222	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)$$
224	221 223	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)$$
225	32	nn0cnd	$$⊢\phi \to K\left(A\cap \left(0..^N\right)\right)\in ℂ$$
226	41	nn0cnd	$$⊢\phi \to K\left(B\cap \left(0..^N\right)\right)\in ℂ$$
227	225 196 226 183	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)$$
228	224 227	eqtrd	$$⊢\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)+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)$$
229	219 228	breq12d	$$⊢\phi \to \left(2^{N+1}\le K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\right)\leftrightarrow 2^N+2^N\le 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)\right)$$
230	213 214 229	3bitr4d	$$⊢\phi \to \left(\varnothing \in C\left(N+1\right)\leftrightarrow 2^{N+1}\le K\left(A\cap \left(0..^N+1\right)\right)+K\left(B\cap \left(0..^N+1\right)\right)\right)$$