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\in {\mathbb{N}}_0$$
	numma.2	$$⊢A\in {\mathbb{N}}_0$$
	numma.3	$$⊢B\in {\mathbb{N}}_0$$
	numma.4	$$⊢C\in {\mathbb{N}}_0$$
	numma.5	$$⊢D\in {\mathbb{N}}_0$$
	numma.6	$$⊢M=TA+B$$
	numma.7	$$⊢N=TC+D$$
	numaddc.8	$$⊢F\in {\mathbb{N}}_0$$
	numaddc.9	$$⊢A+C+1=E$$
	numaddc.10	$$⊢B+D=T\cdot 1+F$$
Assertion	numaddc	$$⊢M+N=TE+F$$

Proof

Step	Hyp	Ref	Expression
1		numma.1	$$⊢T\in {\mathbb{N}}_0$$
2		numma.2	$$⊢A\in {\mathbb{N}}_0$$
3		numma.3	$$⊢B\in {\mathbb{N}}_0$$
4		numma.4	$$⊢C\in {\mathbb{N}}_0$$
5		numma.5	$$⊢D\in {\mathbb{N}}_0$$
6		numma.6	$$⊢M=TA+B$$
7		numma.7	$$⊢N=TC+D$$
8		numaddc.8	$$⊢F\in {\mathbb{N}}_0$$
9		numaddc.9	$$⊢A+C+1=E$$
10		numaddc.10	$$⊢B+D=T\cdot 1+F$$
11	1 2 3	numcl	$$⊢TA+B\in {\mathbb{N}}_0$$
12	6 11	eqeltri	$$⊢M\in {\mathbb{N}}_0$$
13	12	nn0cni	$$⊢M\in ℂ$$
14	13	mulid1i	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1=M$$
15	14	oveq1i	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1+N=M+N$$
16		1nn0	$$⊢1\in {\mathbb{N}}_0$$
17	2	nn0cni	$$⊢A\in ℂ$$
18	17	mulid1i	$$⊢A\cdot 1=A$$
19	18	oveq1i	$$⊢A\cdot 1+C+1=A+C+1$$
20	4	nn0cni	$$⊢C\in ℂ$$
21		ax-1cn	$$⊢1\in ℂ$$
22	17 20 21	addassi	$$⊢A+C+1=A+C+1$$
23	19 22 9	3eqtr2i	$$⊢A\cdot 1+C+1=E$$
24	3	nn0cni	$$⊢B\in ℂ$$
25	24	mulid1i	$$⊢B\cdot 1=B$$
26	25	oveq1i	$$⊢B\cdot 1+D=B+D$$
27	26 10	eqtri	$$⊢B\cdot 1+D=T\cdot 1+F$$
28	1 2 3 4 5 6 7 16 8 16 23 27	nummac	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1+N=TE+F$$
29	15 28	eqtr3i	$$⊢M+N=TE+F$$