Theorem sadasslem

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

	Ref	Expression
Hypotheses	sadasslem.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	sadasslem.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	sadasslem.3	$$⊢\phi \to C\subseteq {\mathbb{N}}_0$$
	sadasslem.4	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	sadasslem	$$⊢\phi \to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		sadasslem.1	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		sadasslem.2	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		sadasslem.3	$$⊢\phi \to C\subseteq {\mathbb{N}}_0$$
4		sadasslem.4	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		inss1	$$⊢A\cap \left(0..^N\right)\subseteq A$$
6	5 1	sstrid	$$⊢\phi \to A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
7		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
8	7	a1i	$$⊢\phi \to \left(0..^N\right)\in \mathrm{Fin}$$
9		inss2	$$⊢A\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
10		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}$$
11	8 9 10	sylancl	$$⊢\phi \to A\cap \left(0..^N\right)\in \mathrm{Fin}$$
12		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)$$
13	6 11 12	sylanbrc	$$⊢\phi \to A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
14		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
15		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$$
16		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$$
17	14 15 16	mp2b	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
18	17	ffvelcdmi	$$⊢A\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
19	13 18	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
20	19	nn0cnd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\in ℂ$$
21		inss1	$$⊢B\cap \left(0..^N\right)\subseteq B$$
22	21 2	sstrid	$$⊢\phi \to B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
23		inss2	$$⊢B\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
24		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}$$
25	8 23 24	sylancl	$$⊢\phi \to B\cap \left(0..^N\right)\in \mathrm{Fin}$$
26		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)$$
27	22 25 26	sylanbrc	$$⊢\phi \to B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
28	17	ffvelcdmi	$$⊢B\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
29	27 28	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
30	29	nn0cnd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\in ℂ$$
31		inss1	$$⊢C\cap \left(0..^N\right)\subseteq C$$
32	31 3	sstrid	$$⊢\phi \to C\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
33		inss2	$$⊢C\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
34		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge C\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to C\cap \left(0..^N\right)\in \mathrm{Fin}$$
35	8 33 34	sylancl	$$⊢\phi \to C\cap \left(0..^N\right)\in \mathrm{Fin}$$
36		elfpw	$$⊢C\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(C\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge C\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
37	32 35 36	sylanbrc	$$⊢\phi \to C\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
38	17	ffvelcdmi	$$⊢C\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
39	37 38	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
40	39	nn0cnd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\in ℂ$$
41	20 30 40	addassd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)$$
42	41	oveq1d	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
43		inss1	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq A\mathrm{sadd}B$$
44		sadcl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
45	1 2 44	syl2anc	$$⊢\phi \to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
46	43 45	sstrid	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
47		inss2	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
48		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}$$
49	8 47 48	sylancl	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
50		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)$$
51	46 49 50	sylanbrc	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
52	17	ffvelcdmi	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
53	51 52	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
54	53	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\in ℝ$$
55	19	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\in ℝ$$
56	29	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\in ℝ$$
57	55 56	readdcld	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\in ℝ$$
58	39	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\in ℝ$$
59		2rp	$$⊢2\in {ℝ}^{+}$$
60	59	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
61	4	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
62	60 61	rpexpcld	$$⊢\phi \to 2^N\in {ℝ}^{+}$$
63		eqid	$$⊢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)=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)$$
64		eqid	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
65	1 2 63 4 64	sadadd3	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
66		eqidd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N$$
67	54 57 58 58 62 65 66	modadd12d	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
68		inss1	$$⊢\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq B\mathrm{sadd}C$$
69		sadcl	$$⊢\left(B\subseteq {\mathbb{N}}_0\wedge C\subseteq {\mathbb{N}}_0\right)\to B\mathrm{sadd}C\subseteq {\mathbb{N}}_0$$
70	2 3 69	syl2anc	$$⊢\phi \to B\mathrm{sadd}C\subseteq {\mathbb{N}}_0$$
71	68 70	sstrid	$$⊢\phi \to \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
72		inss2	$$⊢\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
73		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
74	8 72 73	sylancl	$$⊢\phi \to \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
75		elfpw	$$⊢\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
76	71 74 75	sylanbrc	$$⊢\phi \to \left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
77	17	ffvelcdmi	$$⊢\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
78	76 77	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
79	78	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in ℝ$$
80	56 58	readdcld	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\in ℝ$$
81		eqidd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N$$
82		eqid	$$⊢seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in B,m\in C,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in B,m\in C,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
83	2 3 82 4 64	sadadd3	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
84	55 55 79 80 62 81 83	modadd12d	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
85	42 67 84	3eqtr4d	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
86		eqid	$$⊢seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in \left(A\mathrm{sadd}B\right),m\in C,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in \left(A\mathrm{sadd}B\right),m\in C,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
87	45 3 86 4 64	sadadd3	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(C\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
88		eqid	$$⊢seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in \left(B\mathrm{sadd}C\right),\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in \left(B\mathrm{sadd}C\right),\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
89	1 70 88 4 64	sadadd3	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
90	85 87 89	3eqtr4d	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N$$
91		inss1	$$⊢\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq \left(A\mathrm{sadd}B\right)\mathrm{sadd}C$$
92		sadcl	$$⊢\left(A\mathrm{sadd}B\subseteq {\mathbb{N}}_0\wedge C\subseteq {\mathbb{N}}_0\right)\to \left(A\mathrm{sadd}B\right)\mathrm{sadd}C\subseteq {\mathbb{N}}_0$$
93	45 3 92	syl2anc	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\mathrm{sadd}C\subseteq {\mathbb{N}}_0$$
94	91 93	sstrid	$$⊢\phi \to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
95		inss2	$$⊢\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
96		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
97	8 95 96	sylancl	$$⊢\phi \to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
98		elfpw	$$⊢\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
99	94 97 98	sylanbrc	$$⊢\phi \to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
100	17	ffvelcdmi	$$⊢\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
101	99 100	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
102	101	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in ℝ$$
103	101	nn0ge0d	$$⊢\phi \to 0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)$$
104	101	fvresd	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)=\mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)$$
105		f1ocnvfv2	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\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(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)$$
106	14 99 105	sylancr	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)$$
107	104 106	eqtr3d	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)$$
108	107 95	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
109	101	nn0zd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \mathbb{Z}$$
110		bitsfzo	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
111	109 4 110	syl2anc	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
112	108 111	mpbird	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)$$
113		elfzolt2	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)<2^N$$
114	112 113	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)<2^N$$
115		modid	$$⊢\left(\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\in ℝ\wedge 2^N\in {ℝ}^{+}\right)\wedge \left(0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\wedge {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)<2^N\right)\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)$$
116	102 62 103 114 115	syl22anc	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)$$
117		inss1	$$⊢\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\subseteq A\mathrm{sadd}\left(B\mathrm{sadd}C\right)$$
118		sadcl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\mathrm{sadd}C\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\subseteq {\mathbb{N}}_0$$
119	1 70 118	syl2anc	$$⊢\phi \to A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\subseteq {\mathbb{N}}_0$$
120	117 119	sstrid	$$⊢\phi \to \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
121		inss2	$$⊢\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
122		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
123	8 121 122	sylancl	$$⊢\phi \to \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
124		elfpw	$$⊢\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
125	120 123 124	sylanbrc	$$⊢\phi \to \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
126	17	ffvelcdmi	$$⊢\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
127	125 126	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
128	127	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in ℝ$$
129		2nn	$$⊢2\in \mathbb{N}$$
130	129	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
131	130 4	nnexpcld	$$⊢\phi \to 2^N\in \mathbb{N}$$
132	131	nnrpd	$$⊢\phi \to 2^N\in {ℝ}^{+}$$
133	127	nn0ge0d	$$⊢\phi \to 0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
134	127	fvresd	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)=\mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)$$
135		f1ocnvfv2	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\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(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)$$
136	14 125 135	sylancr	$$⊢\phi \to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)$$
137	134 136	eqtr3d	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)$$
138	137 121	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
139	127	nn0zd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \mathbb{Z}$$
140		bitsfzo	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
141	139 4 140	syl2anc	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
142	138 141	mpbird	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)$$
143		elfzolt2	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)<2^N$$
144	142 143	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)<2^N$$
145		modid	$$⊢\left(\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\in ℝ\wedge 2^N\in {ℝ}^{+}\right)\wedge \left(0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\wedge {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)<2^N\right)\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
146	128 132 133 144 145	syl22anc	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
147	90 116 146	3eqtr3d	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
148		f1of1	$$⊢{\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}\underset{1-1}{⟶}{\mathbb{N}}_0$$
149	14 15 148	mp2b	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1}{⟶}{\mathbb{N}}_0$$
150		f1fveq	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1}{⟶}{\mathbb{N}}_0\wedge \left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\right)\to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
151	149 150	mpan	$$⊢\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge \left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
152	99 125 151	syl2anc	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)\right)$$
153	147 152	mpbid	$$⊢\phi \to \left(\left(A\mathrm{sadd}B\right)\mathrm{sadd}C\right)\cap \left(0..^N\right)=\left(A\mathrm{sadd}\left(B\mathrm{sadd}C\right)\right)\cap \left(0..^N\right)$$