Theorem decaddc2

Description: Add two numerals M and N (with 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
	decaddc.e	|- ( ( A + C ) + 1 ) = E
	decaddc2.t	|- ( B + D ) = ; 1 0
Assertion	decaddc2	|- ( M + N ) = ; E 0

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		decaddc.e	|- ( ( A + C ) + 1 ) = E
8		decaddc2.t	|- ( B + D ) = ; 1 0
9		0nn0	|- 0 e. NN0
10	1 2 3 4 5 6 7 9 8	decaddc	|- ( M + N ) = ; E 0