Metamath Proof Explorer


Theorem dpval2

Description: Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dpval2.a
|- A e. NN0
dpval2.b
|- B e. RR
Assertion dpval2
|- ( A . B ) = ( A + ( B / ; 1 0 ) )

Proof

Step Hyp Ref Expression
1 dpval2.a
 |-  A e. NN0
2 dpval2.b
 |-  B e. RR
3 dpval
 |-  ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B )
4 1 2 3 mp2an
 |-  ( A . B ) = _ A B
5 df-dp2
 |-  _ A B = ( A + ( B / ; 1 0 ) )
6 4 5 eqtri
 |-  ( A . B ) = ( A + ( B / ; 1 0 ) )