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