Definition df-dp2 32859

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12595. (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 32858	. 2 class _𝐴𝐵
4		c1 11014	. . . . 5 class 1
5		cc0 11013	. . . . 5 class 0
6	4, 5	cdc 12594	. . . 4 class ;10
7		cdiv 11781	. . . 4 class /
8	2, 6, 7	co 7352	. . 3 class (𝐵 / ;10)
9		caddc 11016	. . 3 class +
10	1, 8, 9	co 7352	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32860  dp2eq2  32861  dp20u  32865  dp20h  32866  dp2cl  32867  dp2clq  32868  rpdp2cl  32869  dp2lt10  32871  dp2lt  32872  dp2ltsuc  32873  dp2ltc  32874  dpval  32877  dpfrac1  32879  dpval2  32880  dpval3  32881  dp3mul10  32885