Definition df-smu 15198

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

Assertion

Ref	Expression
df-smu	|- smul = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) } )

Distinct variable group:   k, m, n, p, x, y

Detailed syntax breakdown of Definition df-smu

Step	Hyp	Ref	Expression
1		csmu 15143	. 2 class smul
2		vx	. . 3 setvar x
3		vy	. . 3 setvar y
4		cn0 11292	. . . 4 class NN0
5	4	cpw 4158	. . 3 class ~P NN0
6		vk	. . . . . 6 setvar k
7	6	cv 1482	. . . . 5 class k
8		c1 9937	. . . . . . 7 class 1
9		caddc 9939	. . . . . . 7 class +
10	7, 8, 9	co 6650	. . . . . 6 class ( k + 1 )
11		vp	. . . . . . . 8 setvar p
12		vm	. . . . . . . 8 setvar m
13	11	cv 1482	. . . . . . . . 9 class p
14	12, 2	wel 1991	. . . . . . . . . . 11 wff m e. x
15		vn	. . . . . . . . . . . . . 14 setvar n
16	15	cv 1482	. . . . . . . . . . . . 13 class n
17	12	cv 1482	. . . . . . . . . . . . 13 class m
18		cmin 10266	. . . . . . . . . . . . 13 class -
19	16, 17, 18	co 6650	. . . . . . . . . . . 12 class ( n - m )
20	3	cv 1482	. . . . . . . . . . . 12 class y
21	19, 20	wcel 1990	. . . . . . . . . . 11 wff ( n - m ) e. y
22	14, 21	wa 384	. . . . . . . . . 10 wff ( m e. x /\ ( n - m ) e. y )
23	22, 15, 4	crab 2916	. . . . . . . . 9 class { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) }
24		csad 15142	. . . . . . . . 9 class sadd
25	13, 23, 24	co 6650	. . . . . . . 8 class ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } )
26	11, 12, 5, 4, 25	cmpt2 6652	. . . . . . 7 class ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) )
27		cc0 9936	. . . . . . . . . 10 class 0
28	16, 27	wceq 1483	. . . . . . . . 9 wff n = 0
29		c0 3915	. . . . . . . . 9 class (/)
30	16, 8, 18	co 6650	. . . . . . . . 9 class ( n - 1 )
31	28, 29, 30	cif 4086	. . . . . . . 8 class if ( n = 0 , (/) , ( n - 1 ) )
32	15, 4, 31	cmpt 4729	. . . . . . 7 class ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
33	26, 32, 27	cseq 12801	. . . . . 6 class seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
34	10, 33	cfv 5888	. . . . 5 class ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) )
35	7, 34	wcel 1990	. . . 4 wff k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) )
36	35, 6, 4	crab 2916	. . 3 class { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) }
37	2, 3, 5, 5, 36	cmpt2 6652	. 2 class ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) } )
38	1, 37	wceq 1483	1 wff smul = ( x e. ~P NN0 , y e. ~P NN0 |-> { k e. NN0 | k e. ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( k + 1 ) ) } )

This definition is referenced by:  smufval  15199