Theorem sadeq

Description: Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	sadeq.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	sadeq.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	sadeq.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	sadeq	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$

Proof

Step	Hyp	Ref	Expression
1		sadeq.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		sadeq.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		sadeq.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
4		inass	$$⊢\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)=A\cap \left(\left(0..^N\right)\cap \left(0..^N\right)\right)$$
5		inidm	$$⊢\left(0..^N\right)\cap \left(0..^N\right)=\left(0..^N\right)$$
6	5	ineq2i	$$⊢A\cap \left(\left(0..^N\right)\cap \left(0..^N\right)\right)=A\cap \left(0..^N\right)$$
7	4 6	eqtri	$$⊢\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)=A\cap \left(0..^N\right)$$
8	7	fveq2i	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(A\cap \left(0..^N\right)\right)$$
9		inass	$$⊢\left(B\cap \left(0..^N\right)\right)\cap \left(0..^N\right)=B\cap \left(\left(0..^N\right)\cap \left(0..^N\right)\right)$$
10	5	ineq2i	$$⊢B\cap \left(\left(0..^N\right)\cap \left(0..^N\right)\right)=B\cap \left(0..^N\right)$$
11	9 10	eqtri	$$⊢\left(B\cap \left(0..^N\right)\right)\cap \left(0..^N\right)=B\cap \left(0..^N\right)$$
12	11	fveq2i	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(B\cap \left(0..^N\right)\right)$$
13	8 12	oveq12i	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\cap \left(0..^N\right)\right)\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)$$
14	13	oveq1i	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\cap \left(0..^N\right)\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)\right)\mathrm{mod}{2}^N$$
15		inss1	$$⊢A\cap \left(0..^N\right)\subseteq A$$
16	15 1	sstrid	$$⊢\phi \to A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
17		inss1	$$⊢B\cap \left(0..^N\right)\subseteq B$$
18	17 2	sstrid	$$⊢\phi \to B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
19		eqid	$$⊢seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in \left(A\cap \left(0..^N\right)\right),m\in \left(B\cap \left(0..^N\right)\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 \left(A\cap \left(0..^N\right)\right),m\in \left(B\cap \left(0..^N\right)\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)$$
20		eqid	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
21	16 18 19 3 20	sadadd3	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N=\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)+{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(B\cap \left(0..^N\right)\right)\cap \left(0..^N\right)\right)\right)\mathrm{mod}{2}^N$$
22		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)$$
23	1 2 22 3 20	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$$
24	14 21 23	3eqtr4a	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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}B\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N$$
25		inss1	$$⊢\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\subseteq \left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)$$
26		sadcl	$$⊢\left(A\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge B\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\right)\to \left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\subseteq {\mathbb{N}}_0$$
27	16 18 26	syl2anc	$$⊢\phi \to \left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\subseteq {\mathbb{N}}_0$$
28	25 27	sstrid	$$⊢\phi \to \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
29		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
30	29	a1i	$$⊢\phi \to \left(0..^N\right)\in \mathrm{Fin}$$
31		inss2	$$⊢\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
32		ssfi	$$⊢\left(\left(0..^N\right)\in \mathrm{Fin}\wedge \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)\right)\to \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
33	30 31 32	sylancl	$$⊢\phi \to \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
34		elfpw	$$⊢\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\leftrightarrow \left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0\wedge \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\in \mathrm{Fin}\right)$$
35	28 33 34	sylanbrc	$$⊢\phi \to \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
36		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
37		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$$
38		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$$
39	36 37 38	mp2b	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶{\mathbb{N}}_0$$
40	39	ffvelrni	$$⊢\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
41	35 40	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\in {\mathbb{N}}_0$$
42	41	nn0red	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\in ℝ$$
43		2rp	$$⊢2\in {ℝ}^{+}$$
44	43	a1i	$$⊢\phi \to 2\in {ℝ}^{+}$$
45	3	nn0zd	$$⊢\phi \to N\in \mathbb{Z}$$
46	44 45	rpexpcld	$$⊢\phi \to 2^N\in {ℝ}^{+}$$
47	41	nn0ge0d	$$⊢\phi \to 0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
48	41	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\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)=\mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)$$
49		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\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$
50	36 35 49	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\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$
51	48 50	eqtr3d	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$
52	51 31	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
53	41	nn0zd	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\in \mathbb{Z}$$
54		bitsfzo	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
55	53 3 54	syl2anc	$$⊢\phi \to \left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
56	52 55	mpbird	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\in \left(0..^2^N\right)$$
57		elfzolt2	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)<2^N$$
58	56 57	syl	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)<2^N$$
59		modid	$$⊢\left(\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\wedge {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\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\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
60	42 46 47 58 59	syl22anc	$$⊢\phi \to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\mathrm{mod}{2}^N={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
61		inss1	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq A\mathrm{sadd}B$$
62		sadcl	$$⊢\left(A\subseteq {\mathbb{N}}_0\wedge B\subseteq {\mathbb{N}}_0\right)\to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
63	1 2 62	syl2anc	$$⊢\phi \to A\mathrm{sadd}B\subseteq {\mathbb{N}}_0$$
64	61 63	sstrid	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
65		inss2	$$⊢\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\subseteq \left(0..^N\right)$$
66		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}$$
67	30 65 66	sylancl	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \mathrm{Fin}$$
68		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)$$
69	64 67 68	sylanbrc	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)$$
70	39	ffvelrni	$$⊢\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$$
71	69 70	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$$
72	71	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 ℝ$$
73	71	nn0ge0d	$$⊢\phi \to 0\le {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)$$
74	71	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}B\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}B\right)\cap \left(0..^N\right)\right)\right)$$
75		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}B\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}B\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)$$
76	36 69 75	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}B\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)$$
77	74 76	eqtr3d	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\right)=\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)$$
78	77 65	eqsstrdi	$$⊢\phi \to \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)$$
79	71	nn0zd	$$⊢\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{Z}$$
80		bitsfzo	$$⊢\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\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}B\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}B\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
81	79 3 80	syl2anc	$$⊢\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)\in \left(0..^2^N\right)\leftrightarrow \mathrm{bits}\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)\right)\subseteq \left(0..^N\right)\right)$$
82	78 81	mpbird	$$⊢\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 \left(0..^2^N\right)$$
83		elfzolt2	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\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}B\right)\cap \left(0..^N\right)\right)<2^N$$
84	82 83	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)<2^N$$
85		modid	$$⊢\left(\left({\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\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}B\right)\cap \left(0..^N\right)\right)\wedge {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\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}B\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}B\right)\cap \left(0..^N\right)\right)$$
86	72 46 73 84 85	syl22anc	$$⊢\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({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)$$
87	24 60 86	3eqtr3rd	$$⊢\phi \to {\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(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
88		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$$
89	36 37 88	mp2b	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1}{⟶}{\mathbb{N}}_0$$
90		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(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
91	89 90	mpan	$$⊢\left(\left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge \left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\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(A\mathrm{sadd}B\right)\cap \left(0..^N\right)\right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
92	69 35 91	syl2anc	$$⊢\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(\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)\leftrightarrow \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)\right)$$
93	87 92	mpbid	$$⊢\phi \to \left(A\mathrm{sadd}B\right)\cap \left(0..^N\right)=\left(\left(A\cap \left(0..^N\right)\right)\mathrm{sadd}\left(B\cap \left(0..^N\right)\right)\right)\cap \left(0..^N\right)$$