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

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 mulridi ⊢ ( 𝑀 · 1 ) = 𝑀
14 13 oveq1i ⊢ ( ( 𝑀 · 1 ) + 𝑁 ) = ( 𝑀 + 𝑁 )
15 1nn0 ⊢ 1 ∈ ℕ0
16 2 nn0cni ⊢ 𝐴 ∈ ℂ
17 16 mulridi ⊢ ( 𝐴 · 1 ) = 𝐴
18 17 oveq1i ⊢ ( ( 𝐴 · 1 ) + 𝐶 ) = ( 𝐴 + 𝐶 )
19 18 8 eqtri ⊢ ( ( 𝐴 · 1 ) + 𝐶 ) = 𝐸
20 3 nn0cni ⊢ 𝐵 ∈ ℂ
21 20 mulridi ⊢ ( 𝐵 · 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 ⊢ ( 𝑀 + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )