Theorem decaddi

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