Description: Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dp0h.1 | ⊢ 𝐴 ∈ ℝ+ | |
Assertion | dp0h | ⊢ ( 0 . 𝐴 ) = ( 𝐴 / ; 1 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dp0h.1 | ⊢ 𝐴 ∈ ℝ+ | |
2 | 0nn0 | ⊢ 0 ∈ ℕ0 | |
3 | 2 1 | dpval3rp | ⊢ ( 0 . 𝐴 ) = _ 0 𝐴 |
4 | 1 | dp20h | ⊢ _ 0 𝐴 = ( 𝐴 / ; 1 0 ) |
5 | 3 4 | eqtri | ⊢ ( 0 . 𝐴 ) = ( 𝐴 / ; 1 0 ) |