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	addid2i	⊢ ( 0 + 𝐺 ) = 𝐺
14	13	oveq2i	⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐺 ) ) = ( ( 𝐴 · 𝑃 ) + 𝐺 )
15	14 8	eqtri	⊢ ( ( 𝐴 · 𝑃 ) + ( 0 + 𝐺 ) ) = 𝐸
16	1 2 10 3 4 11 5 6 7 15 9	decmac	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ; 𝐸 𝐹