Metamath Proof Explorer

Theorem dp0h

Description: Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypothesis dp0h.1 
|- A e. RR+
Assertion dp0h 
|- ( 0 . A ) = ( A / ; 1 0 )

Proof

Step Hyp Ref Expression
1 dp0h.1 
 |-  A e. RR+
2 0nn0 
 |-  0 e. NN0
3 2 1 dpval3rp 
 |-  ( 0 . A ) = _ 0 A
4 1 dp20h 
 |-  _ 0 A = ( A / ; 1 0 )
5 3 4 eqtri 
 |-  ( 0 . A ) = ( A / ; 1 0 )