Metamath Proof Explorer


Theorem numadd

Description: Add two decimal integers M and N (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 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
numadd.8 ( 𝐴 + 𝐶 ) = 𝐸
numadd.9 ( 𝐵 + 𝐷 ) = 𝐹
Assertion numadd ( 𝑀 + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )

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 numadd.8 ( 𝐴 + 𝐶 ) = 𝐸
9 numadd.9 ( 𝐵 + 𝐷 ) = 𝐹
10 1 2 3 numcl ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0
11 6 10 eqeltri 𝑀 ∈ ℕ0
12 11 nn0cni 𝑀 ∈ ℂ
13 12 mulid1i ( 𝑀 · 1 ) = 𝑀
14 13 oveq1i ( ( 𝑀 · 1 ) + 𝑁 ) = ( 𝑀 + 𝑁 )
15 1nn0 1 ∈ ℕ0
16 2 nn0cni 𝐴 ∈ ℂ
17 16 mulid1i ( 𝐴 · 1 ) = 𝐴
18 17 oveq1i ( ( 𝐴 · 1 ) + 𝐶 ) = ( 𝐴 + 𝐶 )
19 18 8 eqtri ( ( 𝐴 · 1 ) + 𝐶 ) = 𝐸
20 3 nn0cni 𝐵 ∈ ℂ
21 20 mulid1i ( 𝐵 · 1 ) = 𝐵
22 21 oveq1i ( ( 𝐵 · 1 ) + 𝐷 ) = ( 𝐵 + 𝐷 )
23 22 9 eqtri ( ( 𝐵 · 1 ) + 𝐷 ) = 𝐹
24 1 2 3 4 5 6 7 15 19 23 numma ( ( 𝑀 · 1 ) + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )
25 14 24 eqtr3i ( 𝑀 + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )