This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ_{0}$
		decaddi.2	$⊢ B \in ℕ_{0}$
		decaddi.3	$⊢ N \in ℕ_{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 ℕ_{0}$
2		decaddi.2	$⊢ B \in ℕ_{0}$
3		decaddi.3	$⊢ N \in ℕ_{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 ℕ_{0}$
7	3	dec0h	$⊢ N = 0N$
8	1	nn0cni	$⊢ A \in ℂ$
9	8	addridi	$⊢ 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 \|-