Theorem decmac

Description: Perform a multiply-add of two numerals M and N against a fixed multiplicand 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	⊢ 𝑁 = ; 𝐶 𝐷
	decmac.p	⊢ 𝑃 ∈ ℕ0
	decmac.f	⊢ 𝐹 ∈ ℕ0
	decmac.g	⊢ 𝐺 ∈ ℕ0
	decmac.e	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
	decmac.2	⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = ; 𝐺 𝐹
Assertion	decmac	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ; 𝐸 𝐹

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		decmac.p	⊢ 𝑃 ∈ ℕ0
8		decmac.f	⊢ 𝐹 ∈ ℕ0
9		decmac.g	⊢ 𝐺 ∈ ℕ0
10		decmac.e	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
11		decmac.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	nummac	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( ; 1 0 · 𝐸 ) + 𝐹 )
20		dfdec10	⊢ ; 𝐸 𝐹 = ( ( ; 1 0 · 𝐸 ) + 𝐹 )
21	19 20	eqtr4i	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ; 𝐸 𝐹