Theorem decadd

Description: Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decma.a	|- A e. NN0
	decma.b	|- B e. NN0
	decma.c	|- C e. NN0
	decma.d	|- D e. NN0
	decma.m	|- M = ; A B
	decma.n	|- N = ; C D
	decadd.e	|- ( A + C ) = E
	decadd.f	|- ( B + D ) = F
Assertion	decadd	|- ( M + N ) = ; E F

Proof

Step	Hyp	Ref	Expression
1		decma.a	|- A e. NN0
2		decma.b	|- B e. NN0
3		decma.c	|- C e. NN0
4		decma.d	|- D e. NN0
5		decma.m	|- M = ; A B
6		decma.n	|- N = ; C D
7		decadd.e	|- ( A + C ) = E
8		decadd.f	|- ( B + D ) = F
9		10nn0	|- ; 1 0 e. NN0
10		dfdec10	|- ; A B = ( ( ; 1 0 x. A ) + B )
11	5 10	eqtri	|- M = ( ( ; 1 0 x. A ) + B )
12		dfdec10	|- ; C D = ( ( ; 1 0 x. C ) + D )
13	6 12	eqtri	|- N = ( ( ; 1 0 x. C ) + D )
14	9 1 2 3 4 11 13 7 8	numadd	|- ( M + N ) = ( ( ; 1 0 x. E ) + F )
15		dfdec10	|- ; E F = ( ( ; 1 0 x. E ) + F )
16	14 15	eqtr4i	|- ( M + N ) = ; E F