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	⊢ 𝐴 ∈ ℕ
Assertion	decnncl2	⊢ ; 𝐴 0 ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		decnncl2.1	⊢ 𝐴 ∈ ℕ
2		dfdec10	⊢ ; 𝐴 0 = ( ( ; 1 0 · 𝐴 ) + 0 )
3		10nn	⊢ ; 1 0 ∈ ℕ
4	3 1	numnncl2	⊢ ( ( ; 1 0 · 𝐴 ) + 0 ) ∈ ℕ
5	2 4	eqeltri	⊢ ; 𝐴 0 ∈ ℕ