Theorem decaddci

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

	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$$
	decaddci.6	$$⊢C\in {\mathbb{N}}_0$$
	decaddci.7	No typesetting found for |- ( B + N ) = ; 1 C with typecode |-
Assertion	decaddci	Could not format assertion : No typesetting found for |- ( M + N ) = ; D C 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		decaddci.6	$$⊢C\in {\mathbb{N}}_0$$
7		decaddci.7	Could not format ( B + N ) = ; 1 C : No typesetting found for |- ( B + N ) = ; 1 C with typecode |-
8		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9	3	dec0h	$$⊢N=\mathrm{0<mi\; mathcolor="\#808">N</mi>}$$
10	1	nn0cni	$$⊢A\in ℂ$$
11	10	addridi	$$⊢A+0=A$$
12	11	oveq1i	$$⊢A+0+1=A+1$$
13	12 5	eqtri	$$⊢A+0+1=D$$
14	1 2 8 3 4 9 13 6 7	decaddc	Could not format ( M + N ) = ; D C : No typesetting found for |- ( M + N ) = ; D C with typecode |-