Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | numnncl2.1 | |- T e. NN |
|
numnncl2.2 | |- A e. NN |
||
Assertion | numnncl2 | |- ( ( T x. A ) + 0 ) e. NN |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numnncl2.1 | |- T e. NN |
|
2 | numnncl2.2 | |- A e. NN |
|
3 | 1 2 | nnmulcli | |- ( T x. A ) e. NN |
4 | 3 | nncni | |- ( T x. A ) e. CC |
5 | 4 | addid1i | |- ( ( T x. A ) + 0 ) = ( T x. A ) |
6 | 5 3 | eqeltri | |- ( ( T x. A ) + 0 ) e. NN |