Metamath Proof Explorer


Theorem numcl

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

Ref Expression
Hypotheses numnncl.1 𝑇 ∈ ℕ0
numnncl.2 𝐴 ∈ ℕ0
numcl.2 𝐵 ∈ ℕ0
Assertion numcl ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0

Proof

Step Hyp Ref Expression
1 numnncl.1 𝑇 ∈ ℕ0
2 numnncl.2 𝐴 ∈ ℕ0
3 numcl.2 𝐵 ∈ ℕ0
4 1 2 nn0mulcli ( 𝑇 · 𝐴 ) ∈ ℕ0
5 4 3 nn0addcli ( ( 𝑇 · 𝐴 ) + 𝐵 ) ∈ ℕ0