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 A 0
decpmulnc.b B 0
decpmulnc.c C 0
decpmulnc.d D 0
decpmulnc.1 A C = E
decpmulnc.2 A D + B C = F
decpmulnc.3 B D = G
Assertion decpmulnc Could not format assertion : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F G with typecode |-

Proof

Step Hyp Ref Expression
1 decpmulnc.a A 0
2 decpmulnc.b B 0
3 decpmulnc.c C 0
4 decpmulnc.d D 0
5 decpmulnc.1 A C = E
6 decpmulnc.2 A D + B C = F
7 decpmulnc.3 B D = G
8 1 2 deccl Could not format ; A B e. NN0 : No typesetting found for |- ; A B e. NN0 with typecode |-
9 eqid Could not format ; C D = ; C D : No typesetting found for |- ; C D = ; C D with typecode |-
10 2 4 nn0mulcli B D 0
11 7 10 eqeltrri G 0
12 1 4 nn0mulcli A D 0
13 eqid Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
14 12 nn0cni A D
15 2 3 nn0mulcli B C 0
16 15 nn0cni B C
17 14 16 6 addcomli B C + A D = F
18 1 2 12 13 3 5 17 decrmanc Could not format ( ( ; A B x. C ) + ( A x. D ) ) = ; E F : No typesetting found for |- ( ( ; A B x. C ) + ( A x. D ) ) = ; E F with typecode |-
19 eqid A D = A D
20 4 1 2 13 19 7 decmul1 Could not format ( ; A B x. D ) = ; ( A x. D ) G : No typesetting found for |- ( ; A B x. D ) = ; ( A x. D ) G with typecode |-
21 8 3 4 9 11 12 18 20 decmul2c Could not format ( ; A B x. ; C D ) = ; ; E F G : No typesetting found for |- ( ; A B x. ; C D ) = ; ; E F G with typecode |-