Metamath Proof Explorer

Theorem decpmul

Description: Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022)

Ref Expression
Hypotheses decpmulnc.a ⊢ 𝐴 ∈ ℕ0
decpmulnc.b ⊢ 𝐵 ∈ ℕ0
decpmulnc.c ⊢ 𝐶 ∈ ℕ0
decpmulnc.d ⊢ 𝐷 ∈ ℕ0
decpmulnc.1 ⊢ ( 𝐴 · 𝐶 ) = 𝐸
decpmulnc.2 ⊢ ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) = 𝐹
decpmul.3 ⊢ ( 𝐵 · 𝐷 ) = 𝐺 𝐻
decpmul.4 ⊢ ( 𝐸 𝐺 + 𝐹 ) = 𝐼
decpmul.g ⊢ 𝐺 ∈ ℕ0
decpmul.h ⊢ 𝐻 ∈ ℕ0
Assertion decpmul ( 𝐴 𝐵 · 𝐶 𝐷 ) = 𝐼 𝐻

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 decpmul.3 ⊢ ( 𝐵 · 𝐷 ) = 𝐺 𝐻
8 decpmul.4 ⊢ ( 𝐸 𝐺 + 𝐹 ) = 𝐼
9 decpmul.g ⊢ 𝐺 ∈ ℕ0
10 decpmul.h ⊢ 𝐻 ∈ ℕ0
11 1 2 3 4 5 6 7 decpmulnc ⊢ ( 𝐴 𝐵 · 𝐶 𝐷 ) = 𝐸 𝐹 𝐺 𝐻
12 dfdec10 ⊢ 𝐸 𝐹 𝐺 𝐻 = ( ( 1 0 · 𝐸 𝐹 ) + 𝐺 𝐻 )
13 1 3 nn0mulcli ⊢ ( 𝐴 · 𝐶 ) ∈ ℕ0
14 5 13 eqeltrri ⊢ 𝐸 ∈ ℕ0
15 2 3 nn0mulcli ⊢ ( 𝐵 · 𝐶 ) ∈ ℕ0
16 1 4 15 numcl ⊢ ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ∈ ℕ0
17 6 16 eqeltrri ⊢ 𝐹 ∈ ℕ0
18 14 17 deccl ⊢ 𝐸 𝐹 ∈ ℕ0
19 0nn0 ⊢ 0 ∈ ℕ0
20 18 dec0u ⊢ ( 1 0 · 𝐸 𝐹 ) = 𝐸 𝐹 0
21 eqid ⊢ 𝐺 𝐻 = 𝐺 𝐻
22 14 17 9 decaddcom ⊢ ( 𝐸 𝐹 + 𝐺 ) = ( 𝐸 𝐺 + 𝐹 )
23 22 8 eqtri ⊢ ( 𝐸 𝐹 + 𝐺 ) = 𝐼
24 10 nn0cni ⊢ 𝐻 ∈ ℂ
25 24 addid2i ⊢ ( 0 + 𝐻 ) = 𝐻
26 18 19 9 10 20 21 23 25 decadd ⊢ ( ( 1 0 · 𝐸 𝐹 ) + 𝐺 𝐻 ) = 𝐼 𝐻
27 11 12 26 3eqtri ⊢ ( 𝐴 𝐵 · 𝐶 𝐷 ) = 𝐼 𝐻