Metamath Proof Explorer


Theorem numnncl2

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 ) โˆˆ โ„•

Proof

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 ) โˆˆ โ„•