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

Metamath Proof Explorer

Theorem decnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

		Ref	Expression
	Hypothesis	decnncl2.1	$⊢ A \in ℕ$
	Assertion	decnncl2	Could not format assertion : No typesetting found for \|- ; A 0 e. NN with typecode \|-

Step	Hyp	Ref	Expression
1		decnncl2.1	$⊢ A \in ℕ$
2		dfdec10	Could not format ; A 0 = ( ( ; 1 0 x. A ) + 0 ) : No typesetting found for \|- ; A 0 = ( ( ; 1 0 x. A ) + 0 ) with typecode \|-
3		10nn	$⊢ 10 \in ℕ$
4	3 1	numnncl2	$⊢ 10 A + 0 \in ℕ$
5	2 4	eqeltri	Could not format ; A 0 e. NN : No typesetting found for \|- ; A 0 e. NN with typecode \|-