Metamath Proof Explorer

Theorem decma2c

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

Ref Expression
Hypotheses decma.a โŠข ๐ด โˆˆ โ„•0
decma.b โŠข ๐ต โˆˆ โ„•0
decma.c โŠข ๐ถ โˆˆ โ„•0
decma.d โŠข ๐ท โˆˆ โ„•0
decma.m โŠข ๐‘€ = ๐ด ๐ต
decma.n โŠข ๐‘ = ๐ถ ๐ท
decma2c.p โŠข ๐‘ƒ โˆˆ โ„•0
decma2c.f โŠข ๐น โˆˆ โ„•0
decma2c.g โŠข ๐บ โˆˆ โ„•0
decma2c.e โŠข ( ( ๐‘ƒ ยท ๐ด ) + ( ๐ถ + ๐บ ) ) = ๐ธ
decma2c.2 โŠข ( ( ๐‘ƒ ยท ๐ต ) + ๐ท ) = ๐บ ๐น
Assertion decma2c ( ( ๐‘ƒ ยท ๐‘€ ) + ๐‘ ) = ๐ธ ๐น

Proof

Step Hyp Ref Expression
1 decma.a โŠข ๐ด โˆˆ โ„•0
2 decma.b โŠข ๐ต โˆˆ โ„•0
3 decma.c โŠข ๐ถ โˆˆ โ„•0
4 decma.d โŠข ๐ท โˆˆ โ„•0
5 decma.m โŠข ๐‘€ = ๐ด ๐ต
6 decma.n โŠข ๐‘ = ๐ถ ๐ท
7 decma2c.p โŠข ๐‘ƒ โˆˆ โ„•0
8 decma2c.f โŠข ๐น โˆˆ โ„•0
9 decma2c.g โŠข ๐บ โˆˆ โ„•0
10 decma2c.e โŠข ( ( ๐‘ƒ ยท ๐ด ) + ( ๐ถ + ๐บ ) ) = ๐ธ
11 decma2c.2 โŠข ( ( ๐‘ƒ ยท ๐ต ) + ๐ท ) = ๐บ ๐น
12 10nn0 โŠข 1 0 โˆˆ โ„•0
13 dfdec10 โŠข ๐ด ๐ต = ( ( 1 0 ยท ๐ด ) + ๐ต )
14 5 13 eqtri โŠข ๐‘€ = ( ( 1 0 ยท ๐ด ) + ๐ต )
15 dfdec10 โŠข ๐ถ ๐ท = ( ( 1 0 ยท ๐ถ ) + ๐ท )
16 6 15 eqtri โŠข ๐‘ = ( ( 1 0 ยท ๐ถ ) + ๐ท )
17 dfdec10 โŠข ๐บ ๐น = ( ( 1 0 ยท ๐บ ) + ๐น )
18 11 17 eqtri โŠข ( ( ๐‘ƒ ยท ๐ต ) + ๐ท ) = ( ( 1 0 ยท ๐บ ) + ๐น )
19 12 1 2 3 4 14 16 7 8 9 10 18 numma2c โŠข ( ( ๐‘ƒ ยท ๐‘€ ) + ๐‘ ) = ( ( 1 0 ยท ๐ธ ) + ๐น )
20 dfdec10 โŠข ๐ธ ๐น = ( ( 1 0 ยท ๐ธ ) + ๐น )
21 19 20 eqtr4i โŠข ( ( ๐‘ƒ ยท ๐‘€ ) + ๐‘ ) = ๐ธ ๐น