Description: Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | dec0u.1 | |- A e. NN0 |
|
| Assertion | dec0u | |- ( ; 1 0 x. A ) = ; A 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dec0u.1 | |- A e. NN0 |
|
| 2 | 10nn0 | |- ; 1 0 e. NN0 |
|
| 3 | 2 1 | num0u | |- ( ; 1 0 x. A ) = ( ( ; 1 0 x. A ) + 0 ) |
| 4 | dfdec10 | |- ; A 0 = ( ( ; 1 0 x. A ) + 0 ) |
|
| 5 | 3 4 | eqtr4i | |- ( ; 1 0 x. A ) = ; A 0 |