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 โŠข ๐ด โˆˆ โ„•0
decrmanc.b โŠข ๐ต โˆˆ โ„•0
decrmanc.n โŠข ๐‘ โˆˆ โ„•0
decrmanc.m โŠข ๐‘€ = ๐ด ๐ต
decrmanc.p โŠข ๐‘ƒ โˆˆ โ„•0
decrmanc.e โŠข ( ๐ด ยท ๐‘ƒ ) = ๐ธ
decrmanc.f โŠข ( ( ๐ต ยท ๐‘ƒ ) + ๐‘ ) = ๐น
Assertion decrmanc ( ( ๐‘€ ยท ๐‘ƒ ) + ๐‘ ) = ๐ธ ๐น

Proof

Step Hyp Ref Expression
1 decrmanc.a โŠข ๐ด โˆˆ โ„•0
2 decrmanc.b โŠข ๐ต โˆˆ โ„•0
3 decrmanc.n โŠข ๐‘ โˆˆ โ„•0
4 decrmanc.m โŠข ๐‘€ = ๐ด ๐ต
5 decrmanc.p โŠข ๐‘ƒ โˆˆ โ„•0
6 decrmanc.e โŠข ( ๐ด ยท ๐‘ƒ ) = ๐ธ
7 decrmanc.f โŠข ( ( ๐ต ยท ๐‘ƒ ) + ๐‘ ) = ๐น
8 0nn0 โŠข 0 โˆˆ โ„•0
9 3 dec0h โŠข ๐‘ = 0 ๐‘
10 1 5 nn0mulcli โŠข ( ๐ด ยท ๐‘ƒ ) โˆˆ โ„•0
11 10 nn0cni โŠข ( ๐ด ยท ๐‘ƒ ) โˆˆ โ„‚
12 11 addid1i โŠข ( ( ๐ด ยท ๐‘ƒ ) + 0 ) = ( ๐ด ยท ๐‘ƒ )
13 12 6 eqtri โŠข ( ( ๐ด ยท ๐‘ƒ ) + 0 ) = ๐ธ
14 1 2 8 3 4 9 5 13 7 decma โŠข ( ( ๐‘€ ยท ๐‘ƒ ) + ๐‘ ) = ๐ธ ๐น