Description: The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021)(Revised by AV, 6-Sep-2021) Remove hypothesis
D e. NN0 . (Revised by Steven Nguyen, 7-Dec-2022)
Ref
Expression
Hypotheses
decmul1.p
decmul1.a
decmul1.b
decmul1.n
No typesetting found for |- N = ; A B with typecode |-