Theorem smuval

Description: Define the addition of two bit sequences, using df-had and df-cad bit operations. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
	smuval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	smuval	$$⊢\phi \to \left(N\in \left(A\mathrm{smul}B\right)\leftrightarrow N\in P\left(N+1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		smuval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		smuval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		smuval.p	$$⊢P=seq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in A\wedge n-m\in B\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		smuval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5	1 2 3	smufval	$$⊢\phi \to A\mathrm{smul}B=\left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}$$
6	5	eleq2d	$$⊢\phi \to \left(N\in \left(A\mathrm{smul}B\right)\leftrightarrow N\in \left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}\right)$$
7		id	$$⊢k=N\to k=N$$
8		fvoveq1	$$⊢k=N\to P\left(k+1\right)=P\left(N+1\right)$$
9	7 8	eleq12d	$$⊢k=N\to \left(k\in P\left(k+1\right)\leftrightarrow N\in P\left(N+1\right)\right)$$
10	9	elrab3	$$⊢N\in {\mathbb{N}}_0\to \left(N\in \left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}\leftrightarrow N\in P\left(N+1\right)\right)$$
11	4 10	syl	$$⊢\phi \to \left(N\in \left\{k\in {\mathbb{N}}_0|k\in P\left(k+1\right)\right\}\leftrightarrow N\in P\left(N+1\right)\right)$$
12	6 11	bitrd	$$⊢\phi \to \left(N\in \left(A\mathrm{smul}B\right)\leftrightarrow N\in P\left(N+1\right)\right)$$