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

Metamath Proof Explorer

Theorem numma

Description: Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (no 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 ⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
numma.8 ⊢ 𝑃 ∈ ℕ0
numma.9 ⊢ ( ( 𝐴 · 𝑃 ) + 𝐶 ) = 𝐸
numma.10 ⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = 𝐹
Assertion numma ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )

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 numma.8 ⊢ 𝑃 ∈ ℕ0
9 numma.9 ⊢ ( ( 𝐴 · 𝑃 ) + 𝐶 ) = 𝐸
10 numma.10 ⊢ ( ( 𝐵 · 𝑃 ) + 𝐷 ) = 𝐹
11 6 oveq1i ⊢ ( 𝑀 · 𝑃 ) = ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 )
12 11 7 oveq12i ⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) )
13 1 nn0cni ⊢ 𝑇 ∈ ℂ
14 2 nn0cni ⊢ 𝐴 ∈ ℂ
15 8 nn0cni ⊢ 𝑃 ∈ ℂ
16 14 15 mulcli ⊢ ( 𝐴 · 𝑃 ) ∈ ℂ
17 4 nn0cni ⊢ 𝐶 ∈ ℂ
18 13 16 17 adddii ⊢ ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) = ( ( 𝑇 · ( 𝐴 · 𝑃 ) ) + ( 𝑇 · 𝐶 ) )
19 13 14 15 mulassi ⊢ ( ( 𝑇 · 𝐴 ) · 𝑃 ) = ( 𝑇 · ( 𝐴 · 𝑃 ) )
20 19 oveq1i ⊢ ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝑇 · 𝐶 ) ) = ( ( 𝑇 · ( 𝐴 · 𝑃 ) ) + ( 𝑇 · 𝐶 ) )
21 18 20 eqtr4i ⊢ ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) = ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝑇 · 𝐶 ) )
22 21 oveq1i ⊢ ( ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) ) = ( ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝑇 · 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) )
23 13 14 mulcli ⊢ ( 𝑇 · 𝐴 ) ∈ ℂ
24 3 nn0cni ⊢ 𝐵 ∈ ℂ
25 23 24 15 adddiri ⊢ ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 ) = ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝐵 · 𝑃 ) )
26 25 oveq1i ⊢ ( ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) ) = ( ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝐵 · 𝑃 ) ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) )
27 23 15 mulcli ⊢ ( ( 𝑇 · 𝐴 ) · 𝑃 ) ∈ ℂ
28 13 17 mulcli ⊢ ( 𝑇 · 𝐶 ) ∈ ℂ
29 24 15 mulcli ⊢ ( 𝐵 · 𝑃 ) ∈ ℂ
30 5 nn0cni ⊢ 𝐷 ∈ ℂ
31 27 28 29 30 add4i ⊢ ( ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝑇 · 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) ) = ( ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝐵 · 𝑃 ) ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) )
32 26 31 eqtr4i ⊢ ( ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) ) = ( ( ( ( 𝑇 · 𝐴 ) · 𝑃 ) + ( 𝑇 · 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) )
33 22 32 eqtr4i ⊢ ( ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) ) = ( ( ( ( 𝑇 · 𝐴 ) + 𝐵 ) · 𝑃 ) + ( ( 𝑇 · 𝐶 ) + 𝐷 ) )
34 9 oveq2i ⊢ ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) = ( 𝑇 · 𝐸 )
35 34 10 oveq12i ⊢ ( ( 𝑇 · ( ( 𝐴 · 𝑃 ) + 𝐶 ) ) + ( ( 𝐵 · 𝑃 ) + 𝐷 ) ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )
36 12 33 35 3eqtr2i ⊢ ( ( 𝑀 · 𝑃 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )