Theorem decaddci2

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	decaddi.1	$$⊢A\in {\mathbb{N}}_0$$
	decaddi.2	$$⊢B\in {\mathbb{N}}_0$$
	decaddi.3	$$⊢N\in {\mathbb{N}}_0$$
	decaddi.4	No typesetting found for |- M = ; A B with typecode |-
	decaddci.5	$$⊢A+1=D$$
	decaddci2.6	$$⊢B+N=10$$
Assertion	decaddci2	Could not format assertion : No typesetting found for |- ( M + N ) = ; D 0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decaddi.1	$$⊢A\in {\mathbb{N}}_0$$
2		decaddi.2	$$⊢B\in {\mathbb{N}}_0$$
3		decaddi.3	$$⊢N\in {\mathbb{N}}_0$$
4		decaddi.4	Could not format M = ; A B : No typesetting found for |- M = ; A B with typecode |-
5		decaddci.5	$$⊢A+1=D$$
6		decaddci2.6	$$⊢B+N=10$$
7		0nn0	$$⊢0\in {\mathbb{N}}_0$$
8	1 2 3 4 5 7 6	decaddci	Could not format ( M + N ) = ; D 0 : No typesetting found for |- ( M + N ) = ; D 0 with typecode |-