Metamath Proof Explorer

Theorem decrmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by AV, 16-Sep-2021)

Ref Expression
Hypotheses decrmanc.a ⊢ 𝐴 ∈ ℕ0
decrmanc.b ⊢ 𝐵 ∈ ℕ0
decrmanc.n ⊢ 𝑁 ∈ ℕ0
decrmanc.m ⊢ 𝑀 = 𝐴 𝐵
decrmanc.p ⊢ 𝑃 ∈ ℕ0
decrmac.f ⊢ 𝐹 ∈ ℕ0
decrmac.g ⊢ 𝐺 ∈ ℕ0
decrmac.e ⊢ ( ( 𝐴 · 𝑃 ) + 𝐺 ) = 𝐸
decrmac.2 ⊢ ( ( 𝐵 · 𝑃 ) + 𝑁 ) = 𝐺 𝐹
Assertion decrmac ( ( 𝑀 · 𝑃 ) + 𝑁 ) = 𝐸 𝐹

Proof

Step Hyp Ref Expression
1 decrmanc.a ⊢ 𝐴 ∈ ℕ0
2 decrmanc.b ⊢ 𝐵 ∈ ℕ0
3 decrmanc.n ⊢ 𝑁 ∈ ℕ0
4 decrmanc.m ⊢ 𝑀 = 𝐴 𝐵
5 decrmanc.p ⊢ 𝑃 ∈ ℕ0
6 decrmac.f ⊢ 𝐹 ∈ ℕ0
7 decrmac.g ⊢ 𝐺 ∈ ℕ0
8 decrmac.e ⊢ ( ( 𝐴 · 𝑃 ) + 𝐺 ) = 𝐸
9 decrmac.2 ⊢ ( ( 𝐵 · 𝑃 ) + 𝑁 ) = 𝐺 𝐹
10 0nn0 ⊢ 0 ∈ ℕ0
11 3 dec0h ⊢ 𝑁 = 0 𝑁
12 7 nn0cni ⊢ 𝐺 ∈ ℂ
13 12 addlidi ⊢ ( 0 + 𝐺 ) = 𝐺
14 13 oveq2i ⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐺 ) ) = ( ( 𝐴 · 𝑃 ) + 𝐺 )
15 14 8 eqtri ⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐺 ) ) = 𝐸
16 1 2 10 3 4 11 5 6 7 15 9 decmac ⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = 𝐸 𝐹