Theorem dpval2

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

	Ref	Expression
Hypotheses	dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
	dpval2.b	$$⊢B\in ℝ$$
Assertion	dpval2	$$⊢A.B=A+\left(\frac{B}{10}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpval2.b	$$⊢B\in ℝ$$
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+\left(\frac{B}{10}\right)$$