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 \mathbb{N}$$
Assertion	decnncl2	Could not format assertion : No typesetting found for |- ; A 0 e. NN with typecode |-

Proof

Step	Hyp	Ref	Expression
1		decnncl2.1	$$⊢A\in \mathbb{N}$$
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 \mathbb{N}$$
4	3 1	numnncl2	$$⊢10A+0\in \mathbb{N}$$
5	2 4	eqeltri	Could not format ; A 0 e. NN : No typesetting found for |- ; A 0 e. NN with typecode |-