Theorem numnncl2

Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	numnncl2.1	⊢ 𝑇 ∈ ℕ
	numnncl2.2	⊢ 𝐴 ∈ ℕ
Assertion	numnncl2	⊢ ( ( 𝑇 · 𝐴 ) + 0 ) ∈ ℕ

Proof

Step	Hyp	Ref	Expression
1		numnncl2.1	⊢ 𝑇 ∈ ℕ
2		numnncl2.2	⊢ 𝐴 ∈ ℕ
3	1 2	nnmulcli	⊢ ( 𝑇 · 𝐴 ) ∈ ℕ
4	3	nncni	⊢ ( 𝑇 · 𝐴 ) ∈ ℂ
5	4	addid1i	⊢ ( ( 𝑇 · 𝐴 ) + 0 ) = ( 𝑇 · 𝐴 )
6	5 3	eqeltri	⊢ ( ( 𝑇 · 𝐴 ) + 0 ) ∈ ℕ