Metamath Proof Explorer

Theorem decrmanc

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

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

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 decrmanc.e ⊢ ( 𝐴 · 𝑃 ) = 𝐸
7 decrmanc.f ⊢ ( ( 𝐵 · 𝑃 ) + 𝑁 ) = 𝐹
8 0nn0 ⊢ 0 ∈ ℕ0
9 3 dec0h ⊢ 𝑁 = 0 𝑁
10 1 5 nn0mulcli ⊢ ( 𝐴 · 𝑃 ) ∈ ℕ0
11 10 nn0cni ⊢ ( 𝐴 · 𝑃 ) ∈ ℂ
12 11 addid1i ⊢ ( ( 𝐴 · 𝑃 ) + 0 ) = ( 𝐴 · 𝑃 )
13 12 6 eqtri ⊢ ( ( 𝐴 · 𝑃 ) + 0 ) = 𝐸
14 1 2 8 3 4 9 5 13 7 decma ⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = 𝐸 𝐹