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	|- _ A B = ( A + ( B / ; 1 0 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cdp2	|- _ A B
3		caddc	|- +
4		cdiv	|- /
5		c1	|- 1
6		cc0	|- 0
7	5 6	cdc	|- ; 1 0
8	1 7 4	co	|- ( B / ; 1 0 )
9	0 8 3	co	|- ( A + ( B / ; 1 0 ) )
10	2 9	wceq	|- _ A B = ( A + ( B / ; 1 0 ) )