Description: Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | numnncl2.1 | โข ๐ โ โ | |
numnncl2.2 | โข ๐ด โ โ | ||
Assertion | numnncl2 | โข ( ( ๐ ยท ๐ด ) + 0 ) โ โ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numnncl2.1 | โข ๐ โ โ | |
2 | numnncl2.2 | โข ๐ด โ โ | |
3 | 1 2 | nnmulcli | โข ( ๐ ยท ๐ด ) โ โ |
4 | 3 | nncni | โข ( ๐ ยท ๐ด ) โ โ |
5 | 4 | addridi | โข ( ( ๐ ยท ๐ด ) + 0 ) = ( ๐ ยท ๐ด ) |
6 | 5 3 | eqeltri | โข ( ( ๐ ยท ๐ด ) + 0 ) โ โ |