Definition df-dp2 32847

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12586. (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 32846	. 2 class _𝐴𝐵
4		c1 11004	. . . . 5 class 1
5		cc0 11003	. . . . 5 class 0
6	4, 5	cdc 12585	. . . 4 class ;10
7		cdiv 11771	. . . 4 class /
8	2, 6, 7	co 7346	. . 3 class (𝐵 / ;10)
9		caddc 11006	. . 3 class +
10	1, 8, 9	co 7346	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32848  dp2eq2  32849  dp20u  32853  dp20h  32854  dp2cl  32855  dp2clq  32856  rpdp2cl  32857  dp2lt10  32859  dp2lt  32860  dp2ltsuc  32861  dp2ltc  32862  dpval  32865  dpfrac1  32867  dpval2  32868  dpval3  32869  dp3mul10  32873