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 ⊢ 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
numadd.8 ⊢ A + C = E
numadd.9 ⊢ B + D = F
Assertion numadd ⊢ M + 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 numadd.8 ⊢ A + C = E
9 numadd.9 ⊢ B + D = F
10 1 2 3 numcl ⊢ T ⁢ A + B ∈ ℕ 0
11 6 10 eqeltri ⊢ M ∈ ℕ 0
12 11 nn0cni ⊢ M ∈ ℂ
13 12 mulridi ⊢ M ⋅ 1 = M
14 13 oveq1i ⊢ M ⋅ 1 + N = M + N
15 1nn0 ⊢ 1 ∈ ℕ 0
16 2 nn0cni ⊢ A ∈ ℂ
17 16 mulridi ⊢ A ⋅ 1 = A
18 17 oveq1i ⊢ A ⋅ 1 + C = A + C
19 18 8 eqtri ⊢ A ⋅ 1 + C = E
20 3 nn0cni ⊢ B ∈ ℂ
21 20 mulridi ⊢ B ⋅ 1 = B
22 21 oveq1i ⊢ B ⋅ 1 + D = B + D
23 22 9 eqtri ⊢ B ⋅ 1 + D = F
24 1 2 3 4 5 6 7 15 19 23 numma ⊢ M ⋅ 1 + N = T ⁢ E + F
25 14 24 eqtr3i ⊢ M + N = T ⁢ E + F