Metamath Proof Explorer

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 
|- 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csmu 
 |-  smul
1 vx 
 |-  x
2 cn0 
 |-  NN0
3 2 cpw 
 |-  ~P NN0
4 vy 
 |-  y
5 vk 
 |-  k
6 5 cv 
 |-  k
7 cc0 
 |-  0
8 vp 
 |-  p
9 vm 
 |-  m
10 8 cv 
 |-  p
11 csad 
 |-  sadd
12 vn 
 |-  n
13 9 cv 
 |-  m
14 1 cv 
 |-  x
15 13 14 wcel 
 |-  m e. x
16 12 cv 
 |-  n
17 cmin 
 |-  -
18 16 13 17 co 
 |-  ( n - m )
19 4 cv 
 |-  y
20 18 19 wcel 
 |-  ( n - m ) e. y
21 15 20 wa 
 |-  ( m e. x /\ ( n - m ) e. y )
22 21 12 2 crab 
 |-  { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) }
23 10 22 11 co 
 |-  ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } )
24 8 9 3 2 23 cmpo 
 |-  ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. x /\ ( n - m ) e. y ) } ) )
25 16 7 wceq 
 |-  n = 0
26 c0 
 |-  (/)
27 c1 
 |-  1
28 16 27 17 co 
 |-  ( n - 1 )
29 25 26 28 cif 
 |-  if ( n = 0 , (/) , ( n - 1 ) )
30 12 2 29 cmpt 
 |-  ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) )
31 24 30 7 cseq 
 |-  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 ) ) ) )
32 caddc 
 |-  +
33 6 27 32 co 
 |-  ( k + 1 )
34 33 31 cfv 
 |-  ( 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 6 34 wcel 
 |-  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 5 2 crab 
 |-  { 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 1 4 3 3 36 cmpo 
 |-  ( 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 0 37 wceq 
 |-  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 ) ) } )