Metamath Proof Explorer

Theorem dp0u

Description: Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypothesis dp0u.1 
|- A e. NN0
Assertion dp0u 
|- ( A . 0 ) = A

Proof

Step Hyp Ref Expression
1 dp0u.1 
 |-  A e. NN0
2 0re 
 |-  0 e. RR
3 1 2 dpval3 
 |-  ( A . 0 ) = _ A 0
4 1 dp20u 
 |-  _ A 0 = A
5 3 4 eqtri 
 |-  ( A . 0 ) = A