Metamath Proof Explorer


Theorem decnncl

Description: Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses decnncl.1 โŠข ๐ด โˆˆ โ„•0
decnncl.2 โŠข ๐ต โˆˆ โ„•
Assertion decnncl ๐ด ๐ต โˆˆ โ„•

Proof

Step Hyp Ref Expression
1 decnncl.1 โŠข ๐ด โˆˆ โ„•0
2 decnncl.2 โŠข ๐ต โˆˆ โ„•
3 dfdec10 โŠข ๐ด ๐ต = ( ( 1 0 ยท ๐ด ) + ๐ต )
4 10nn0 โŠข 1 0 โˆˆ โ„•0
5 4 1 2 numnncl โŠข ( ( 1 0 ยท ๐ด ) + ๐ต ) โˆˆ โ„•
6 3 5 eqeltri โŠข ๐ด ๐ต โˆˆ โ„•