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\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$$
	numadd.8	$$⊢A+C=E$$
	numadd.9	$$⊢B+D=F$$
Assertion	numadd	$$⊢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		numadd.8	$$⊢A+C=E$$
9		numadd.9	$$⊢B+D=F$$
10	1 2 3	numcl	$$⊢TA+B\in {\mathbb{N}}_0$$
11	6 10	eqeltri	$$⊢M\in {\mathbb{N}}_0$$
12	11	nn0cni	$$⊢M\in ℂ$$
13	12	mulridi	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1=M$$
14	13	oveq1i	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1+N=M+N$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16	2	nn0cni	$$⊢A\in ℂ$$
17	16	mulridi	$$⊢A\cdot 1=A$$
18	17	oveq1i	$$⊢A\cdot 1+C=A+C$$
19	18 8	eqtri	$$⊢A\cdot 1+C=E$$
20	3	nn0cni	$$⊢B\in ℂ$$
21	20	mulridi	$$⊢B\cdot 1=B$$
22	21	oveq1i	$$⊢B\cdot 1+D=B+D$$
23	22 9	eqtri	$$⊢B\cdot 1+D=F$$
24	1 2 3 4 5 6 7 15 19 23	numma	$$⊢\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot 1+N=TE+F$$
25	14 24	eqtr3i	$$⊢M+N=TE+F$$