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