Definition df-dp2 29578

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

Assertion

Ref	Expression
df-dp2	|- _ A B = ( A + ( B / ; 1 0 ) )

Detailed syntax breakdown of Definition df-dp2

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cdp2 29577	. 2 class _ A B
4		c1 9937	. . . . 5 class 1
5		cc0 9936	. . . . 5 class 0
6	4, 5	cdc 11493	. . . 4 class ; 1 0
7		cdiv 10684	. . . 4 class /
8	2, 6, 7	co 6650	. . 3 class ( B / ; 1 0 )
9		caddc 9939	. . 3 class +
10	1, 8, 9	co 6650	. 2 class ( A + ( B / ; 1 0 ) )
11	3, 10	wceq 1483	1 wff _ A B = ( A + ( B / ; 1 0 ) )

This definition is referenced by:  dfdp2OLD  29579  dp2eq1  29580  dp2eq2  29581  dp20u  29585  dp20h  29586  dp2cl  29587  dp2clq  29588  rpdp2cl  29589  dp2lt10  29591  dp2lt  29592  dp2ltsuc  29593  dp2ltc  29594  dpval  29597  dpfrac1  29599  dpval2  29601  dpval3  29602  dp3mul10  29606