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

Metamath Proof Explorer

Theorem numaddc

Description: Add two decimal integers M and N (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
numaddc.8 ⊢ F ∈ ℕ 0
numaddc.9 ⊢ A + C + 1 = E
numaddc.10 ⊢ B + D = T ⋅ 1 + F
Assertion numaddc ⊢ 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 numaddc.8 ⊢ F ∈ ℕ 0
9 numaddc.9 ⊢ A + C + 1 = E
10 numaddc.10 ⊢ B + D = T ⋅ 1 + F
11 1 2 3 numcl ⊢ T ⁢ A + B ∈ ℕ 0
12 6 11 eqeltri ⊢ M ∈ ℕ 0
13 12 nn0cni ⊢ M ∈ ℂ
14 13 mulridi ⊢ M ⋅ 1 = M
15 14 oveq1i ⊢ M ⋅ 1 + N = M + N
16 1nn0 ⊢ 1 ∈ ℕ 0
17 2 nn0cni ⊢ A ∈ ℂ
18 17 mulridi ⊢ A ⋅ 1 = A
19 18 oveq1i ⊢ A ⋅ 1 + C + 1 = A + C + 1
20 4 nn0cni ⊢ C ∈ ℂ
21 ax-1cn ⊢ 1 ∈ ℂ
22 17 20 21 addassi ⊢ A + C + 1 = A + C + 1
23 19 22 9 3eqtr2i ⊢ A ⋅ 1 + C + 1 = E
24 3 nn0cni ⊢ B ∈ ℂ
25 24 mulridi ⊢ B ⋅ 1 = B
26 25 oveq1i ⊢ B ⋅ 1 + D = B + D
27 26 10 eqtri ⊢ B ⋅ 1 + D = T ⋅ 1 + F
28 1 2 3 4 5 6 7 16 8 16 23 27 nummac ⊢ M ⋅ 1 + N = T ⁢ E + F
29 15 28 eqtr3i ⊢ M + N = T ⁢ E + F