Theorem numma2c

Description: Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014)

	Ref	Expression
Hypotheses	numma.1	⊢ 𝑇 ∈ ℕ0
	numma.2	⊢ 𝐴 ∈ ℕ0
	numma.3	⊢ 𝐵 ∈ ℕ0
	numma.4	⊢ 𝐶 ∈ ℕ0
	numma.5	⊢ 𝐷 ∈ ℕ0
	numma.6	⊢ 𝑀 = ( ( 𝑇 · 𝐴 ) + 𝐵 )
	numma.7	⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
	numma2c.8	⊢ 𝑃 ∈ ℕ0
	numma2c.9	⊢ 𝐹 ∈ ℕ0
	numma2c.10	⊢ 𝐺 ∈ ℕ0
	numma2c.11	⊢ ( ( 𝑃 · 𝐴 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
	numma2c.12	⊢ ( ( 𝑃 · 𝐵 ) + 𝐷 ) = ( ( 𝑇 · 𝐺 ) + 𝐹 )
Assertion	numma2c	⊢ ( ( 𝑃 · 𝑀 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		numma.1	⊢ 𝑇 ∈ ℕ0
2		numma.2	⊢ 𝐴 ∈ ℕ0
3		numma.3	⊢ 𝐵 ∈ ℕ0
4		numma.4	⊢ 𝐶 ∈ ℕ0
5		numma.5	⊢ 𝐷 ∈ ℕ0
6		numma.6	⊢ 𝑀 = ( ( 𝑇 · 𝐴 ) + 𝐵 )
7		numma.7	⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
8		numma2c.8	⊢ 𝑃 ∈ ℕ0
9		numma2c.9	⊢ 𝐹 ∈ ℕ0
10		numma2c.10	⊢ 𝐺 ∈ ℕ0
11		numma2c.11	⊢ ( ( 𝑃 · 𝐴 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
12		numma2c.12	⊢ ( ( 𝑃 · 𝐵 ) + 𝐷 ) = ( ( 𝑇 · 𝐺 ) + 𝐹 )
13	8	nn0cni	⊢ 𝑃 ∈ ℂ
14	1 2 3	numcl	⊢ ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0
15	6 14	eqeltri	⊢ 𝑀 ∈ ℕ0
16	15	nn0cni	⊢ 𝑀 ∈ ℂ
17	13 16	mulcomi	⊢ ( 𝑃 · 𝑀 ) = ( 𝑀 · 𝑃 )
18	17	oveq1i	⊢ ( ( 𝑃 · 𝑀 ) + 𝑁 ) = ( ( 𝑀 · 𝑃 ) + 𝑁 )
19	2	nn0cni	⊢ 𝐴 ∈ ℂ
20	19 13	mulcomi	⊢ ( 𝐴 · 𝑃 ) = ( 𝑃 · 𝐴 )
21	20	oveq1i	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = ( ( 𝑃 · 𝐴 ) + ( 𝐶 + 𝐺 ) )
22	21 11	eqtri	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
23	3	nn0cni	⊢ 𝐵 ∈ ℂ
24	23 13	mulcomi	⊢ ( 𝐵 · 𝑃 ) = ( 𝑃 · 𝐵 )
25	24	oveq1i	⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = ( ( 𝑃 · 𝐵 ) + 𝐷 )
26	25 12	eqtri	⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = ( ( 𝑇 · 𝐺 ) + 𝐹 )
27	1 2 3 4 5 6 7 8 9 10 22 26	nummac	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )
28	18 27	eqtri	⊢ ( ( 𝑃 · 𝑀 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )