Definition df-dp2 32781

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12734. (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 32780	. 2 class _𝐴𝐵
4		c1 11160	. . . . 5 class 1
5		cc0 11159	. . . . 5 class 0
6	4, 5	cdc 12733	. . . 4 class ;10
7		cdiv 11922	. . . 4 class /
8	2, 6, 7	co 7427	. . 3 class (𝐵 / ;10)
9		caddc 11162	. . 3 class +
10	1, 8, 9	co 7427	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1534	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32782  dp2eq2  32783  dp20u  32787  dp20h  32788  dp2cl  32789  dp2clq  32790  rpdp2cl  32791  dp2lt10  32793  dp2lt  32794  dp2ltsuc  32795  dp2ltc  32796  dpval  32799  dpfrac1  32801  dpval2  32802  dpval3  32803  dp3mul10  32807