Definition df-dp2 32931

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12645. (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 32930	. 2 class _𝐴𝐵
4		c1 11039	. . . . 5 class 1
5		cc0 11038	. . . . 5 class 0
6	4, 5	cdc 12644	. . . 4 class ;10
7		cdiv 11807	. . . 4 class /
8	2, 6, 7	co 7367	. . 3 class (𝐵 / ;10)
9		caddc 11041	. . 3 class +
10	1, 8, 9	co 7367	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1542	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32932  dp2eq2  32933  dp20u  32937  dp20h  32938  dp2cl  32939  dp2clq  32940  rpdp2cl  32941  dp2lt10  32943  dp2lt  32944  dp2ltsuc  32945  dp2ltc  32946  dpval  32949  dpfrac1  32951  dpval2  32952  dpval3  32953  dp3mul10  32957