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

Metamath Proof Explorer

Theorem numnncl2

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

Step	Hyp	Ref	Expression
1		numnncl2.1	$⊢ T \in ℕ$
2		numnncl2.2	$⊢ A \in ℕ$
3	1 2	nnmulcli	$⊢ T A \in ℕ$
4	3	nncni	$⊢ T A \in ℂ$
5	4	addridi	$⊢ T A + 0 = T A$
6	5 3	eqeltri	$⊢ T A + 0 \in ℕ$