This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )