Theorem dpval3rp

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

	Ref	Expression
Hypotheses	dpval3rp.a	|- A e. NN0
	dpval3rp.b	|- B e. RR+
Assertion	dpval3rp	|- ( A . B ) = _ A B

Proof

Step	Hyp	Ref	Expression
1		dpval3rp.a	|- A e. NN0
2		dpval3rp.b	|- B e. RR+
3		rpre	|- ( B e. RR+ -> B e. RR )
4	2 3	ax-mp	|- B e. RR
5	1 4	dpval3	|- ( A . B ) = _ A B