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

Theorem smufval 14425
 Description: The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.)
Hypotheses
Ref Expression
smuval.a
smuval.b
Assertion
Ref Expression
smufval smul
Distinct variable groups:   ,,,,   ,,   ,,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem smufval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smuval.a . . 3
2 nn0ex 10875 . . . 4
32elpw2 4589 . . 3
41, 3sylibr 215 . 2
5 smuval.b . . 3
62elpw2 4589 . . 3
75, 6sylibr 215 . 2
8 simp1l 1029 . . . . . . . . . . . . 13
98eleq2d 2499 . . . . . . . . . . . 12
10 simp1r 1030 . . . . . . . . . . . . 13
1110eleq2d 2499 . . . . . . . . . . . 12
129, 11anbi12d 715 . . . . . . . . . . 11
1312rabbidv 3079 . . . . . . . . . 10
1413oveq2d 6321 . . . . . . . . 9 sadd sadd
1514mpt2eq3dva 6369 . . . . . . . 8 sadd sadd