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

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 ∈ ℕ 0
dpval2.b ⊢ B ∈ ℝ
Assertion dpval2 ⊢ A . B = A + B 10

Proof

Step Hyp Ref Expression
1 dpval2.a ⊢ A ∈ ℕ 0
2 dpval2.b ⊢ B ∈ ℝ
3 dpval Could not format ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) : No typesetting found for |- ( ( A e. NN0 /\ B e. RR ) -> ( A . B ) = _ A B ) with typecode |-
4 1 2 3 mp2an Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-
5 df-dp2 Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
6 4 5 eqtri ⊢ A . B = A + B 10