This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. NN0
decpmulnc.b 
|- B e. NN0
decpmulnc.c 
|- C e. NN0
decpmulnc.d 
|- D e. NN0
decpmulnc.1 
|- ( A x. C ) = E
decpmulnc.2 
|- ( ( A x. D ) + ( B x. C ) ) = F
decpmulnc.3 
|- ( B x. D ) = G
Assertion decpmulnc 
|- ( ; A B x. ; C D ) = ; ; E F G

Proof

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