Metamath Proof Explorer

Theorem decma2c

Description: Perform a multiply-add of two numerals M and N against a fixed multiplier P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decma.a ⊢ 𝐴 ∈ ℕ0
decma.b ⊢ 𝐵 ∈ ℕ0
decma.c ⊢ 𝐶 ∈ ℕ0
decma.d ⊢ 𝐷 ∈ ℕ0
decma.m ⊢ 𝑀 = 𝐴 𝐵
decma.n ⊢ 𝑁 = 𝐶 𝐷
decma2c.p ⊢ 𝑃 ∈ ℕ0
decma2c.f ⊢ 𝐹 ∈ ℕ0
decma2c.g ⊢ 𝐺 ∈ ℕ0
decma2c.e ⊢ ( ( 𝑃 · 𝐴 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
decma2c.2 ⊢ ( ( 𝑃 · 𝐵 ) + 𝐷 ) = 𝐺 𝐹
Assertion decma2c ( ( 𝑃 · 𝑀 ) + 𝑁 ) = 𝐸 𝐹

Proof

Step Hyp Ref Expression
1 decma.a ⊢ 𝐴 ∈ ℕ0
2 decma.b ⊢ 𝐵 ∈ ℕ0
3 decma.c ⊢ 𝐶 ∈ ℕ0
4 decma.d ⊢ 𝐷 ∈ ℕ0
5 decma.m ⊢ 𝑀 = 𝐴 𝐵
6 decma.n ⊢ 𝑁 = 𝐶 𝐷
7 decma2c.p ⊢ 𝑃 ∈ ℕ0
8 decma2c.f ⊢ 𝐹 ∈ ℕ0
9 decma2c.g ⊢ 𝐺 ∈ ℕ0
10 decma2c.e ⊢ ( ( 𝑃 · 𝐴 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
11 decma2c.2 ⊢ ( ( 𝑃 · 𝐵 ) + 𝐷 ) = 𝐺 𝐹
12 10nn0 ⊢ 1 0 ∈ ℕ0
13 dfdec10 ⊢ 𝐴 𝐵 = ( ( 1 0 · 𝐴 ) + 𝐵 )
14 5 13 eqtri ⊢ 𝑀 = ( ( 1 0 · 𝐴 ) + 𝐵 )
15 dfdec10 ⊢ 𝐶 𝐷 = ( ( 1 0 · 𝐶 ) + 𝐷 )
16 6 15 eqtri ⊢ 𝑁 = ( ( 1 0 · 𝐶 ) + 𝐷 )
17 dfdec10 ⊢ 𝐺 𝐹 = ( ( 1 0 · 𝐺 ) + 𝐹 )
18 11 17 eqtri ⊢ ( ( 𝑃 · 𝐵 ) + 𝐷 ) = ( ( 1 0 · 𝐺 ) + 𝐹 )
19 12 1 2 3 4 14 16 7 8 9 10 18 numma2c ⊢ ( ( 𝑃 · 𝑀 ) + 𝑁 ) = ( ( 1 0 · 𝐸 ) + 𝐹 )
20 dfdec10 ⊢ 𝐸 𝐹 = ( ( 1 0 · 𝐸 ) + 𝐹 )
21 19 20 eqtr4i ⊢ ( ( 𝑃 · 𝑀 ) + 𝑁 ) = 𝐸 𝐹