This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpval3

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

Ref Expression
Hypotheses dpval2.a ⊢ 𝐴 ∈ ℕ0
dpval2.b ⊢ 𝐵 ∈ ℝ
Assertion dpval3 ( 𝐴 . 𝐵 ) = 𝐴 𝐵

Proof

Step Hyp Ref Expression
1 dpval2.a ⊢ 𝐴 ∈ ℕ0
2 dpval2.b ⊢ 𝐵 ∈ ℝ
3 1 2 dpval2 ⊢ ( 𝐴 . 𝐵 ) = ( 𝐴 + ( 𝐵 / 1 0 ) )
4 df-dp2 ⊢ 𝐴 𝐵 = ( 𝐴 + ( 𝐵 / 1 0 ) )
5 3 4 eqtr4i ⊢ ( 𝐴 . 𝐵 ) = 𝐴 𝐵