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 ⊢ ( 𝐴 𝐵 · 𝐶 𝐷 ) = 𝐸 𝐹 𝐺