Definition df-dp2 33420

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12796. (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 33419	. 2 class _𝐴𝐵
4		c1 11182	. . . . 5 class 1
5		cc0 11181	. . . . 5 class 0
6	4, 5	cdc 12795	. . . 4 class ;10
7		cdiv 11954	. . . 4 class /
8	2, 6, 7	co 7412	. . 3 class (𝐵 / ;10)
9		caddc 11184	. . 3 class +
10	1, 8, 9	co 7412	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1570	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is used by:  dp2eq1  33421  dp2eq2  33422  dp20u  33426  dp20h  33427  dp2cl  33428  dp2clq  33429  rpdp2cl  33430  dp2lt10  33432  dp2lt  33433  dp2ltsuc  33434  dp2ltc  33435  dpval  33438  dpfrac1  33440  dpval2  33441  dpval3  33442  dp3mul10  33446