Definition df-dp2

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec . (Contributed by David A. Wheeler, 15-May-2015) (Revised by AV, 9-Sep-2021)

	Ref	Expression
Assertion	df-dp2	Could not format assertion : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cdp2	Could not format _ A B : No typesetting found for class _ A B with typecode class
3		caddc	$$class+$$
4		cdiv	$$class÷$$
5		c1	$$class1$$
6		cc0	$$class0$$
7	5 6	cdc	$$class10$$
8	1 7 4	co	$$class\left(\frac{B}{10}\right)$$
9	0 8 3	co	$$class\left(A+\left(\frac{B}{10}\right)\right)$$
10	2 9	wceq	Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for wff _ A B = ( A + ( B / ; 1 0 ) ) with typecode wff