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 ⊢ 𝑇 ∈ ℕ0
numma.2 ⊢ 𝐴 ∈ ℕ0
numma.3 ⊢ 𝐵 ∈ ℕ0
numma.4 ⊢ 𝐶 ∈ ℕ0
numma.5 ⊢ 𝐷 ∈ ℕ0
numma.6 ⊢ 𝑀 = ( ( 𝑇 · 𝐴 ) + 𝐵 )
numma.7 ⊢ 𝑁 = ( ( 𝑇 · 𝐶 ) + 𝐷 )
numaddc.8 ⊢ 𝐹 ∈ ℕ0
numaddc.9 ⊢ ( ( 𝐴 + 𝐶 ) + 1 ) = 𝐸
numaddc.10 ⊢ ( 𝐵 + 𝐷 ) = ( ( 𝑇 · 1 ) + 𝐹 )
Assertion numaddc ( 𝑀 + 𝑁 ) = ( ( 𝑇 · 𝐸 ) + 𝐹 )

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