Definition df-dp2 33508

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12842. (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 33507	. 2 class _𝐴𝐵
4		c1 11228	. . . . 5 class 1
5		cc0 11227	. . . . 5 class 0
6	4, 5	cdc 12841	. . . 4 class ;10
7		cdiv 12000	. . . 4 class /
8	2, 6, 7	co 7443	. . 3 class (𝐵 / ;10)
9		caddc 11230	. . 3 class +
10	1, 8, 9	co 7443	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1570	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is used by:  dp2eq1  33509  dp2eq2  33510  dp20u  33514  dp20h  33515  dp2cl  33516  dp2clq  33517  rpdp2cl  33518  dp2lt10  33520  dp2lt  33521  dp2ltsuc  33522  dp2ltc  33523  dpval  33526  dpfrac1  33528  dpval2  33529  dpval3  33530  dp3mul10  33534