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

Metamath Proof Explorer

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 ℕ_{0}$
	decaddi.2	$⊢ B \in ℕ_{0}$
	decaddi.3	$⊢ N \in ℕ_{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 \|-

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		decaddci.5	$⊢ A + 1 = D$
6		decaddci2.6	$⊢ B + N = 10$
7		0nn0	$⊢ 0 \in ℕ_{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 \|-