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

Definition df-smu 12980
 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 sadd
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-smu
StepHypRef Expression
1 csmu 12925 . 2 smul
2 vx . . 3
3 vy . . 3
4 cn0 10213 . . . 4
54cpw 3791 . . 3
6 vk . . . . . 6
76cv 1651 . . . . 5
8 c1 8983 . . . . . . 7
9 caddc 8985 . . . . . . 7
107, 8, 9co 6073 . . . . . 6
11 vp . . . . . . . 8
12 vm . . . . . . . 8
1311cv 1651 . . . . . . . . 9
1412, 2wel 1726 . . . . . . . . . . 11
15 vn . . . . . . . . . . . . . 14
1615cv 1651 . . . . . . . . . . . . 13
1712cv 1651 . . . . . . . . . . . . 13
18 cmin 9283 . . . . . . . . . . . . 13
1916, 17, 18co 6073 . . . . . . . . . . . 12
203cv 1651 . . . . . . . . . . . 12
2119, 20wcel 1725 . . . . . . . . . . 11
2214, 21wa 359 . . . . . . . . . 10
2322, 15, 4crab 2701 . . . . . . . . 9
24 csad 12924 . . . . . . . . 9 sadd
2513, 23, 24co 6073 . . . . . . . 8 sadd
2611, 12, 5, 4, 25cmpt2 6075 . . . . . . 7 sadd
27 cc0 8982 . . . . . . . . . 10
2816, 27wceq 1652 . . . . . . . . 9
29 c0 3620 . . . . . . . . 9
3016, 8, 18co 6073 . . . . . . . . 9
3128, 29, 30cif 3731 . . . . . . . 8
3215, 4, 31cmpt 4258 . . . . . . 7
3326, 32, 27cseq 11315 . . . . . 6 sadd
3410, 33cfv 5446 . . . . 5 sadd
357, 34wcel 1725 . . . 4 sadd
3635, 6, 4crab 2701 . . 3 sadd
372, 3, 5, 5, 36cmpt2 6075 . 2 sadd
381, 37wceq 1652 1 smul sadd
 Colors of variables: wff set class This definition is referenced by:  smufval  12981
 Copyright terms: Public domain W3C validator