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\in {\mathbb{N}}_0$$
	decma.b	$$⊢B\in {\mathbb{N}}_0$$
	decma.c	$$⊢C\in {\mathbb{N}}_0$$
	decma.d	$$⊢D\in {\mathbb{N}}_0$$
	decma.m	No typesetting found for |- M = ; A B with typecode |-
	decma.n	No typesetting found for |- N = ; C D with typecode |-
	decaddc.e	$$⊢A+C+1=E$$
	decaddc2.t	$$⊢B+D=10$$
Assertion	decaddc2	Could not format assertion : No typesetting found for |- ( M + N ) = ; E 0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decma.a	$$⊢A\in {\mathbb{N}}_0$$
2		decma.b	$$⊢B\in {\mathbb{N}}_0$$
3		decma.c	$$⊢C\in {\mathbb{N}}_0$$
4		decma.d	$$⊢D\in {\mathbb{N}}_0$$
5		decma.m	Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
6		decma.n	Could not format N = ; C D : No typesetting found for |- N = ; C D with typecode |-
7		decaddc.e	$$⊢A+C+1=E$$
8		decaddc2.t	$$⊢B+D=10$$
9		0nn0	$$⊢0\in {\mathbb{N}}_0$$
10	1 2 3 4 5 6 7 9 8	decaddc	Could not format ( M + N ) = ; E 0 : No typesetting found for |- ( M + N ) = ; E 0 with typecode |-