Theorem nummac

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	⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
	nummac.8	⊢ 𝑃 ∈ ℕ0
	nummac.9	⊢ 𝐹 ∈ ℕ0
	nummac.10	⊢ 𝐺 ∈ ℕ0
	nummac.11	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
	nummac.12	⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = ( ( 𝑇 · 𝐺 ) + 𝐹 )
Assertion	nummac	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )

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		nummac.8	⊢ 𝑃 ∈ ℕ0
9		nummac.9	⊢ 𝐹 ∈ ℕ0
10		nummac.10	⊢ 𝐺 ∈ ℕ0
11		nummac.11	⊢ ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) ) = 𝐸
12		nummac.12	⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = ( ( 𝑇 · 𝐺 ) + 𝐹 )
13	1	nn0cni	⊢ 𝑇 ∈ ℂ
14	2	nn0cni	⊢ 𝐴 ∈ ℂ
15	8	nn0cni	⊢ 𝑃 ∈ ℂ
16	14 15	mulcli	⊢ ( 𝐴 · 𝑃 ) ∈ ℂ
17	4	nn0cni	⊢ 𝐶 ∈ ℂ
18	10	nn0cni	⊢ 𝐺 ∈ ℂ
19	16 17 18	addassi	⊢ ( ( ( 𝐴 · 𝑃 ) + 𝐶 ) + 𝐺 ) = ( ( 𝐴 · 𝑃 ) + ( 𝐶 + 𝐺 ) )
20	19 11	eqtri	⊢ ( ( ( 𝐴 · 𝑃 ) + 𝐶 ) + 𝐺 ) = 𝐸
21	16 17	addcli	⊢ ( ( 𝐴 · 𝑃 ) + 𝐶 ) ∈ ℂ
22	21 18	addcli	⊢ ( ( ( 𝐴 · 𝑃 ) + 𝐶 ) + 𝐺 ) ∈ ℂ
23	20 22	eqeltrri	⊢ 𝐸 ∈ ℂ
24	13 23 18	subdii	⊢ ( 𝑇 · ( 𝐸 − 𝐺 ) ) = ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) )
25	24	oveq1i	⊢ ( ( 𝑇 · ( 𝐸 − 𝐺 ) ) + ( ( 𝑇 · 𝐺 ) + 𝐹 ) ) = ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( ( 𝑇 · 𝐺 ) + 𝐹 ) )
26	23 18 21	subadd2i	⊢ ( ( 𝐸 − 𝐺 ) = ( ( 𝐴 · 𝑃 ) + 𝐶 ) ↔ ( ( ( 𝐴 · 𝑃 ) + 𝐶 ) + 𝐺 ) = 𝐸 )
27	20 26	mpbir	⊢ ( 𝐸 − 𝐺 ) = ( ( 𝐴 · 𝑃 ) + 𝐶 )
28	27	eqcomi	⊢ ( ( 𝐴 · 𝑃 ) + 𝐶 ) = ( 𝐸 − 𝐺 )
29	1 2 3 4 5 6 7 8 28 12	numma	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · ( 𝐸 − 𝐺 ) ) + ( ( 𝑇 · 𝐺 ) + 𝐹 ) )
30	13 23	mulcli	⊢ ( 𝑇 · 𝐸 ) ∈ ℂ
31	13 18	mulcli	⊢ ( 𝑇 · 𝐺 ) ∈ ℂ
32		npcan	⊢ ( ( ( 𝑇 · 𝐸 ) ∈ ℂ ∧ ( 𝑇 · 𝐺 ) ∈ ℂ ) → ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( 𝑇 · 𝐺 ) ) = ( 𝑇 · 𝐸 ) )
33	30 31 32	mp2an	⊢ ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( 𝑇 · 𝐺 ) ) = ( 𝑇 · 𝐸 )
34	33	oveq1i	⊢ ( ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( 𝑇 · 𝐺 ) ) + 𝐹 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )
35	30 31	subcli	⊢ ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) ∈ ℂ
36	9	nn0cni	⊢ 𝐹 ∈ ℂ
37	35 31 36	addassi	⊢ ( ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( 𝑇 · 𝐺 ) ) + 𝐹 ) = ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( ( 𝑇 · 𝐺 ) + 𝐹 ) )
38	34 37	eqtr3i	⊢ ( ( 𝑇 · 𝐸 ) + 𝐹 ) = ( ( ( 𝑇 · 𝐸 ) − ( 𝑇 · 𝐺 ) ) + ( ( 𝑇 · 𝐺 ) + 𝐹 ) )
39	25 29 38	3eqtr4i	⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )