Metamath Proof Explorer


Theorem decmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decma.a A0
decma.b B0
decma.c C0
decma.d D0
decma.m No typesetting found for |- M = ; A B with typecode |-
decma.n No typesetting found for |- N = ; C D with typecode |-
decmac.p P0
decmac.f F0
decmac.g G0
decmac.e AP+C+G=E
decmac.2 No typesetting found for |- ( ( B x. P ) + D ) = ; G F with typecode |-
Assertion decmac Could not format assertion : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-

Proof

Step Hyp Ref Expression
1 decma.a A0
2 decma.b B0
3 decma.c C0
4 decma.d D0
5 decma.m Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
6 decma.n Could not format N = ; C D : No typesetting found for |- N = ; C D with typecode |-
7 decmac.p P0
8 decmac.f F0
9 decmac.g G0
10 decmac.e AP+C+G=E
11 decmac.2 Could not format ( ( B x. P ) + D ) = ; G F : No typesetting found for |- ( ( B x. P ) + D ) = ; G F with typecode |-
12 10nn0 100
13 dfdec10 Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
14 5 13 eqtri M=10A+B
15 dfdec10 Could not format ; C D = ( ( ; 1 0 x. C ) + D ) : No typesetting found for |- ; C D = ( ( ; 1 0 x. C ) + D ) with typecode |-
16 6 15 eqtri N=10C+D
17 dfdec10 Could not format ; G F = ( ( ; 1 0 x. G ) + F ) : No typesetting found for |- ; G F = ( ( ; 1 0 x. G ) + F ) with typecode |-
18 11 17 eqtri BP+D=10G+F
19 12 1 2 3 4 14 16 7 8 9 10 18 nummac MP+N=10E+F
20 dfdec10 Could not format ; E F = ( ( ; 1 0 x. E ) + F ) : No typesetting found for |- ; E F = ( ( ; 1 0 x. E ) + F ) with typecode |-
21 19 20 eqtr4i Could not format ( ( M x. P ) + N ) = ; E F : No typesetting found for |- ( ( M x. P ) + N ) = ; E F with typecode |-