Definition df-smu

Description: Define the multiplication of two bit sequences, using repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Assertion	df-smu	$$⊢\mathrm{smul}=\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|k\in 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 x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmu	$$class\mathrm{smul}$$
1		vx	$$setvarx$$
2		cn0	$$class{\mathbb{N}}_0$$
3	2	cpw	$$class𝒫{\mathbb{N}}_0$$
4		vy	$$setvary$$
5		vk	$$setvark$$
6	5	cv	$$setvark$$
7		cc0	$$class0$$
8		vp	$$setvarp$$
9		vm	$$setvarm$$
10	8	cv	$$setvarp$$
11		csad	$$class\mathrm{sadd}$$
12		vn	$$setvarn$$
13	9	cv	$$setvarm$$
14	1	cv	$$setvarx$$
15	13 14	wcel	$$wffm\in x$$
16	12	cv	$$setvarn$$
17		cmin	$$class-$$
18	16 13 17	co	$$class\left(n-m\right)$$
19	4	cv	$$setvary$$
20	18 19	wcel	$$wffn-m\in y$$
21	15 20	wa	$$wff\left(m\in x\wedge n-m\in y\right)$$
22	21 12 2	crab	$$class\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}$$
23	10 22 11	co	$$class\left(p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right)$$
24	8 9 3 2 23	cmpo	$$class\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right)$$
25	16 7	wceq	$$wffn=0$$
26		c0	$$class\varnothing$$
27		c1	$$class1$$
28	16 27 17	co	$$class\left(n-1\right)$$
29	25 26 28	cif	$$classif\left(n=0,\varnothing ,n-1\right)$$
30	12 2 29	cmpt	$$class\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)$$
31	24 30 7	cseq	$$classseq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
32		caddc	$$class+$$
33	6 27 32	co	$$class\left(k+1\right)$$
34	33 31	cfv	$$classseq0\left(\left(p\in 𝒫{\mathbb{N}}_0,m\in {\mathbb{N}}_0⟼p\mathrm{sadd}\left\{n\in {\mathbb{N}}_0|\left(m\in x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)$$
35	6 34	wcel	$$wffk\in 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 x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)$$
36	35 5 2	crab	$$class\left\{k\in {\mathbb{N}}_0|k\in 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 x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}$$
37	1 4 3 3 36	cmpo	$$class\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|k\in 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 x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}\right)$$
38	0 37	wceq	$$wff\mathrm{smul}=\left(x\in 𝒫{\mathbb{N}}_0,y\in 𝒫{\mathbb{N}}_0⟼\left\{k\in {\mathbb{N}}_0|k\in 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 x\wedge n-m\in y\right)\right\}\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)\left(k+1\right)\right\}\right)$$