Metamath Proof Explorer
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 |
โข ; ๐ด ๐ต โ โ |