MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-smu Unicode version

Definition df-smu 12667
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
StepHypRef Expression
1 csmu 12612 . 2  class smul
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cn0 9965 . . . 4  class  NN0
54cpw 3625 . . 3  class  ~P NN0
6 vk . . . . . 6  set  k
76cv 1622 . . . . 5  class  k
8 c1 8738 . . . . . . 7  class  1
9 caddc 8740 . . . . . . 7  class  +
107, 8, 9co 5858 . . . . . 6  class  ( k  +  1 )
11 vp . . . . . . . 8  set  p
12 vm . . . . . . . 8  set  m
1311cv 1622 . . . . . . . . 9  class  p
1412, 2wel 1685 . . . . . . . . . . 11  wff  m  e.  x
15 vn . . . . . . . . . . . . . 14  set  n
1615cv 1622 . . . . . . . . . . . . 13  class  n
1712cv 1622 . . . . . . . . . . . . 13  class  m
18 cmin 9037 . . . . . . . . . . . . 13  class  -
1916, 17, 18co 5858 . . . . . . . . . . . 12  class  ( n  -  m )
203cv 1622 . . . . . . . . . . . 12  class  y
2119, 20wcel 1684 . . . . . . . . . . 11  wff  ( n  -  m )  e.  y
2214, 21wa 358 . . . . . . . . . 10  wff  ( m  e.  x  /\  (
n  -  m )  e.  y )
2322, 15, 4crab 2547 . . . . . . . . 9  class  { n  e.  NN0  |  ( m  e.  x  /\  (
n  -  m )  e.  y ) }
24 csad 12611 . . . . . . . . 9  class sadd
2513, 23, 24co 5858 . . . . . . . 8  class  ( p sadd  { n  e.  NN0  |  ( m  e.  x  /\  ( n  -  m
)  e.  y ) } )
2611, 12, 5, 4, 25cmpt2 5860 . . . . . . 7  class  ( p  e.  ~P NN0 ,  m  e.  NN0  |->  ( p sadd  { n  e.  NN0  |  ( m  e.  x  /\  ( n  -  m
)  e.  y ) } ) )
27 cc0 8737 . . . . . . . . . 10  class  0
2816, 27wceq 1623 . . . . . . . . 9  wff  n  =  0
29 c0 3455 . . . . . . . . 9  class  (/)
3016, 8, 18co 5858 . . . . . . . . 9  class  ( n  -  1 )
3128, 29, 30cif 3565 . . . . . . . 8  class  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) )
3215, 4, 31cmpt 4077 . . . . . . 7  class  ( n  e.  NN0  |->  if ( n  =  0 ,  (/) ,  ( n  - 
1 ) ) )
3326, 32, 27cseq 11046 . . . . . 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 ) ) ) )
3410, 33cfv 5255 . . . . 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 ) )
357, 34wcel 1684 . . . 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 ) )
3635, 6, 4crab 2547 . . 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 ) ) }
372, 3, 5, 5, 36cmpt2 5860 . 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 ) ) } )
381, 37wceq 1623 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 ) ) } )
Colors of variables: wff set class
This definition is referenced by:  smufval  12668
  Copyright terms: Public domain W3C validator