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

Metamath Proof Explorer

Theorem numnncl

Description: Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses numnncl.1 ⊢ T ∈ ℕ 0
numnncl.2 ⊢ A ∈ ℕ 0
numnncl.3 ⊢ B ∈ ℕ
Assertion numnncl ⊢ T ⁢ A + B ∈ ℕ

Proof

Step Hyp Ref Expression
1 numnncl.1 ⊢ T ∈ ℕ 0
2 numnncl.2 ⊢ A ∈ ℕ 0
3 numnncl.3 ⊢ B ∈ ℕ
4 1 2 nn0mulcli ⊢ T ⁢ A ∈ ℕ 0
5 nn0nnaddcl ⊢ T ⁢ A ∈ ℕ 0 ∧ B ∈ ℕ → T ⁢ A + B ∈ ℕ
6 4 3 5 mp2an ⊢ T ⁢ A + B ∈ ℕ