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