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

Metamath Proof Explorer

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