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

Definition df-smu 14126
Description: Define the multiplication of two bit sequences, using repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.)
Assertion
Ref Expression
df-smu
Distinct variable group:   , , , , ,

Detailed syntax breakdown of Definition df-smu
StepHypRef Expression
1 csmu 14071 . 2
2 vx . . 3
3 vy . . 3
4 cn0 10820 . . . 4
54cpw 4012 . . 3
6 vk . . . . . 6
76cv 1394 . . . . 5
8 c1 9514 . . . . . . 7
9 caddc 9516 . . . . . . 7
107, 8, 9co 6296 . . . . . 6
11 vp . . . . . . . 8
12 vm . . . . . . . 8
1311cv 1394 . . . . . . . . 9
1412, 2wel 1819 . . . . . . . . . . 11
15 vn . . . . . . . . . . . . . 14
1615cv 1394 . . . . . . . . . . . . 13
1712cv 1394 . . . . . . . . . . . . 13
18 cmin 9828 . . . . . . . . . . . . 13
1916, 17, 18co 6296 . . . . . . . . . . . 12
203cv 1394 . . . . . . . . . . . 12
2119, 20wcel 1818 . . . . . . . . . . 11
2214, 21wa 369 . . . . . . . . . 10
2322, 15, 4crab 2811 . . . . . . . . 9
24 csad 14070 . . . . . . . . 9
2513, 23, 24co 6296 . . . . . . . 8
2611, 12, 5, 4, 25cmpt2 6298 . . . . . . 7
27 cc0 9513 . . . . . . . . . 10
2816, 27wceq 1395 . . . . . . . . 9
29 c0 3784 . . . . . . . . 9
3016, 8, 18co 6296 . . . . . . . . 9
3128, 29, 30cif 3941 . . . . . . . 8
3215, 4, 31cmpt 4510 . . . . . . 7
3326, 32, 27cseq 12107 . . . . . 6
3410, 33cfv 5593 . . . . 5
357, 34wcel 1818 . . . 4
3635, 6, 4crab 2811 . . 3
372, 3, 5, 5, 36cmpt2 6298 . 2
381, 37wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  smufval  14127
  Copyright terms: Public domain W3C validator