Metamath Proof Explorer

Theorem decpmulnc

Description: Partial products algorithm for two digit multiplication, no carry. Compare muladdi . (Contributed by Steven Nguyen, 9-Dec-2022)

Ref Expression
Hypotheses decpmulnc.a โŠข ๐ด โˆˆ โ„•0
decpmulnc.b โŠข ๐ต โˆˆ โ„•0
decpmulnc.c โŠข ๐ถ โˆˆ โ„•0
decpmulnc.d โŠข ๐ท โˆˆ โ„•0
decpmulnc.1 โŠข ( ๐ด ยท ๐ถ ) = ๐ธ
decpmulnc.2 โŠข ( ( ๐ด ยท ๐ท ) + ( ๐ต ยท ๐ถ ) ) = ๐น
decpmulnc.3 โŠข ( ๐ต ยท ๐ท ) = ๐บ
Assertion decpmulnc ( ๐ด ๐ต ยท ๐ถ ๐ท ) = ๐ธ ๐น ๐บ

Proof

Step Hyp Ref Expression
1 decpmulnc.a โŠข ๐ด โˆˆ โ„•0
2 decpmulnc.b โŠข ๐ต โˆˆ โ„•0
3 decpmulnc.c โŠข ๐ถ โˆˆ โ„•0
4 decpmulnc.d โŠข ๐ท โˆˆ โ„•0
5 decpmulnc.1 โŠข ( ๐ด ยท ๐ถ ) = ๐ธ
6 decpmulnc.2 โŠข ( ( ๐ด ยท ๐ท ) + ( ๐ต ยท ๐ถ ) ) = ๐น
7 decpmulnc.3 โŠข ( ๐ต ยท ๐ท ) = ๐บ
8 1 2 deccl โŠข ๐ด ๐ต โˆˆ โ„•0
9 eqid โŠข ๐ถ ๐ท = ๐ถ ๐ท
10 2 4 nn0mulcli โŠข ( ๐ต ยท ๐ท ) โˆˆ โ„•0
11 7 10 eqeltrri โŠข ๐บ โˆˆ โ„•0
12 1 4 nn0mulcli โŠข ( ๐ด ยท ๐ท ) โˆˆ โ„•0
13 eqid โŠข ๐ด ๐ต = ๐ด ๐ต
14 12 nn0cni โŠข ( ๐ด ยท ๐ท ) โˆˆ โ„‚
15 2 3 nn0mulcli โŠข ( ๐ต ยท ๐ถ ) โˆˆ โ„•0
16 15 nn0cni โŠข ( ๐ต ยท ๐ถ ) โˆˆ โ„‚
17 14 16 6 addcomli โŠข ( ( ๐ต ยท ๐ถ ) + ( ๐ด ยท ๐ท ) ) = ๐น
18 1 2 12 13 3 5 17 decrmanc โŠข ( ( ๐ด ๐ต ยท ๐ถ ) + ( ๐ด ยท ๐ท ) ) = ๐ธ ๐น
19 eqid โŠข ( ๐ด ยท ๐ท ) = ( ๐ด ยท ๐ท )
20 4 1 2 13 19 7 decmul1 โŠข ( ๐ด ๐ต ยท ๐ท ) = ( ๐ด ยท ๐ท ) ๐บ
21 8 3 4 9 11 12 18 20 decmul2c โŠข ( ๐ด ๐ต ยท ๐ถ ๐ท ) = ๐ธ ๐น ๐บ