Theorem dpval3

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	dpval3	Could not format assertion : No typesetting found for |- ( A . B ) = _ A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpval2.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpval2.b	$$⊢B\in ℝ$$
3	1 2	dpval2	$$⊢A.B=A+\left(\frac{B}{10}\right)$$
4		df-dp2	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
5	3 4	eqtr4i	Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-