Definition df-dp2 33104

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

Assertion

Ref	Expression
df-dp2	⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

Detailed syntax breakdown of Definition df-dp2

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cdp2 33103	. 2 class _𝐴𝐵
4		c1 11089	. . . . 5 class 1
5		cc0 11088	. . . . 5 class 0
6	4, 5	cdc 12702	. . . 4 class ;10
7		cdiv 11859	. . . 4 class /
8	2, 6, 7	co 7400	. . 3 class (𝐵 / ;10)
9		caddc 11091	. . 3 class +
10	1, 8, 9	co 7400	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1563	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  33105  dp2eq2  33106  dp20u  33110  dp20h  33111  dp2cl  33112  dp2clq  33113  rpdp2cl  33114  dp2lt10  33116  dp2lt  33117  dp2ltsuc  33118  dp2ltc  33119  dpval  33122  dpfrac1  33124  dpval2  33125  dpval3  33126  dp3mul10  33130