Metamath Proof Explorer


Theorem decrmanc

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no carry). (Contributed by AV, 16-Sep-2021)

Ref Expression
Hypotheses decrmanc.a A0
decrmanc.b B0
decrmanc.n N0
decrmanc.m No typesetting found for |- M = ; A B with typecode |-
decrmanc.p P0
decrmanc.e AP=E
decrmanc.f BP+N=F
Assertion decrmanc Could not format assertion : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-

Proof

Step Hyp Ref Expression
1 decrmanc.a A0
2 decrmanc.b B0
3 decrmanc.n N0
4 decrmanc.m Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
5 decrmanc.p P0
6 decrmanc.e AP=E
7 decrmanc.f BP+N=F
8 0nn0 00
9 3 dec0h N=0 N
10 1 5 nn0mulcli AP0
11 10 nn0cni AP
12 11 addid1i AP+0=AP
13 12 6 eqtri AP+0=E
14 1 2 8 3 4 9 5 13 7 decma Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-