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 | ⊢ 𝐴 ∈ ℕ0 | |
| Assertion | dec0h | ⊢ 𝐴 = ; 0 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dec0u.1 | ⊢ 𝐴 ∈ ℕ0 | |
| 2 | 10nn0 | ⊢ ; 1 0 ∈ ℕ0 | |
| 3 | 2 1 | num0h | ⊢ 𝐴 = ( ( ; 1 0 · 0 ) + 𝐴 ) |
| 4 | dfdec10 | ⊢ ; 0 𝐴 = ( ( ; 1 0 · 0 ) + 𝐴 ) | |
| 5 | 3 4 | eqtr4i | ⊢ 𝐴 = ; 0 𝐴 |