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 ⊢ T ∈ ℕ 0
numma.2 ⊢ A ∈ ℕ 0
numma.3 ⊢ B ∈ ℕ 0
numma.4 ⊢ C ∈ ℕ 0
numma.5 ⊢ D ∈ ℕ 0
numma.6 ⊢ M = T ⁢ A + B
numma.7 ⊢ N = T ⁢ C + D
nummac.8 ⊢ P ∈ ℕ 0
nummac.9 ⊢ F ∈ ℕ 0
nummac.10 ⊢ G ∈ ℕ 0
nummac.11 ⊢ A ⁢ P + C + G = E
nummac.12 ⊢ B ⁢ P + D = T ⁢ G + F
Assertion nummac ⊢ M ⁢ P + N = T ⁢ E + F

Proof

Step Hyp Ref Expression
1 numma.1 ⊢ T ∈ ℕ 0
2 numma.2 ⊢ A ∈ ℕ 0
3 numma.3 ⊢ B ∈ ℕ 0
4 numma.4 ⊢ C ∈ ℕ 0
5 numma.5 ⊢ D ∈ ℕ 0
6 numma.6 ⊢ M = T ⁢ A + B
7 numma.7 ⊢ N = T ⁢ C + D
8 nummac.8 ⊢ P ∈ ℕ 0
9 nummac.9 ⊢ F ∈ ℕ 0
10 nummac.10 ⊢ G ∈ ℕ 0
11 nummac.11 ⊢ A ⁢ P + C + G = E
12 nummac.12 ⊢ B ⁢ P + D = T ⁢ G + F
13 1 nn0cni ⊢ T ∈ ℂ
14 2 nn0cni ⊢ A ∈ ℂ
15 8 nn0cni ⊢ P ∈ ℂ
16 14 15 mulcli ⊢ A ⁢ P ∈ ℂ
17 4 nn0cni ⊢ C ∈ ℂ
18 10 nn0cni ⊢ G ∈ ℂ
19 16 17 18 addassi ⊢ A ⁢ P + C + G = A ⁢ P + C + G
20 19 11 eqtri ⊢ A ⁢ P + C + G = E
21 16 17 addcli ⊢ A ⁢ P + C ∈ ℂ
22 21 18 addcli ⊢ A ⁢ P + C + G ∈ ℂ
23 20 22 eqeltrri ⊢ E ∈ ℂ
24 13 23 18 subdii ⊢ T ⁢ E − G = T ⁢ E − T ⁢ G
25 24 oveq1i ⊢ T ⁢ E − G + T ⁢ G + F = T ⁢ E − T ⁢ G + T ⁢ G + F
26 23 18 21 subadd2i ⊢ E − G = A ⁢ P + C ↔ A ⁢ P + C + G = E
27 20 26 mpbir ⊢ E − G = A ⁢ P + C
28 27 eqcomi ⊢ A ⁢ P + C = E − G
29 1 2 3 4 5 6 7 8 28 12 numma ⊢ M ⁢ P + N = T ⁢ E − G + T ⁢ G + F
30 13 23 mulcli ⊢ T ⁢ E ∈ ℂ
31 13 18 mulcli ⊢ T ⁢ G ∈ ℂ
32 npcan ⊢ T ⁢ E ∈ ℂ ∧ T ⁢ G ∈ ℂ → T ⁢ E - T ⁢ G + T ⁢ G = T ⁢ E
33 30 31 32 mp2an ⊢ T ⁢ E - T ⁢ G + T ⁢ G = T ⁢ E
34 33 oveq1i ⊢ T ⁢ E − T ⁢ G + T ⁢ G + F = T ⁢ E + F
35 30 31 subcli ⊢ T ⁢ E − T ⁢ G ∈ ℂ
36 9 nn0cni ⊢ F ∈ ℂ
37 35 31 36 addassi ⊢ T ⁢ E − T ⁢ G + T ⁢ G + F = T ⁢ E − T ⁢ G + T ⁢ G + F
38 34 37 eqtr3i ⊢ T ⁢ E + F = T ⁢ E − T ⁢ G + T ⁢ G + F
39 25 29 38 3eqtr4i ⊢ M ⁢ P + N = T ⁢ E + F