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

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

Detailed syntax breakdown of Definition df-smu
StepHypRef Expression
1 csmu 12888 . 2 smul
2 vx . . 3
3 vy . . 3
4 cn0 10177 . . . 4
54cpw 3759 . . 3
6 vk . . . . . 6
76cv 1648 . . . . 5
8 c1 8947 . . . . . . 7
9 caddc 8949 . . . . . . 7
107, 8, 9co 6040 . . . . . 6
11 vp . . . . . . . 8
12 vm . . . . . . . 8
1311cv 1648 . . . . . . . . 9
1412, 2wel 1722 . . . . . . . . . . 11
15 vn . . . . . . . . . . . . . 14
1615cv 1648 . . . . . . . . . . . . 13
1712cv 1648 . . . . . . . . . . . . 13
18 cmin 9247 . . . . . . . . . . . . 13
1916, 17, 18co 6040 . . . . . . . . . . . 12
203cv 1648 . . . . . . . . . . . 12
2119, 20wcel 1721 . . . . . . . . . . 11
2214, 21wa 359 . . . . . . . . . 10
2322, 15, 4crab 2670 . . . . . . . . 9
24 csad 12887 . . . . . . . . 9 sadd
2513, 23, 24co 6040 . . . . . . . 8 sadd
2611, 12, 5, 4, 25cmpt2 6042 . . . . . . 7 sadd
27 cc0 8946 . . . . . . . . . 10
2816, 27wceq 1649 . . . . . . . . 9
29 c0 3588 . . . . . . . . 9
3016, 8, 18co 6040 . . . . . . . . 9
3128, 29, 30cif 3699 . . . . . . . 8
3215, 4, 31cmpt 4226 . . . . . . 7
3326, 32, 27cseq 11278 . . . . . 6 sadd
3410, 33cfv 5413 . . . . 5 sadd
357, 34wcel 1721 . . . 4 sadd
3635, 6, 4crab 2670 . . 3 sadd
372, 3, 5, 5, 36cmpt2 6042 . 2 sadd
381, 37wceq 1649 1 smul sadd
 Colors of variables: wff set class This definition is referenced by:  smufval  12944
 Copyright terms: Public domain W3C validator