Metamath Proof Explorer


Theorem dpval2

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

Ref Expression
Hypotheses dpval2.a 𝐴 ∈ ℕ0
dpval2.b 𝐵 ∈ ℝ
Assertion dpval2 ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / 1 0 ) )

Proof

Step Hyp Ref Expression
1 dpval2.a 𝐴 ∈ ℕ0
2 dpval2.b 𝐵 ∈ ℝ
3 dpval ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )
4 1 2 3 mp2an ( 𝐴 . 𝐵 ) = 𝐴 𝐵
5 df-dp2 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
6 4 5 eqtri ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / 1 0 ) )