Definition df-dp2 30548

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12098. (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 30547	. 2 class _𝐴𝐵
4		c1 10537	. . . . 5 class 1
5		cc0 10536	. . . . 5 class 0
6	4, 5	cdc 12097	. . . 4 class ;10
7		cdiv 11296	. . . 4 class /
8	2, 6, 7	co 7155	. . 3 class (𝐵 / ;10)
9		caddc 10539	. . 3 class +
10	1, 8, 9	co 7155	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1533	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  30549  dp2eq2  30550  dp20u  30554  dp20h  30555  dp2cl  30556  dp2clq  30557  rpdp2cl  30558  dp2lt10  30560  dp2lt  30561  dp2ltsuc  30562  dp2ltc  30563  dpval  30566  dpfrac1  30568  dpval2  30569  dpval3  30570  dp3mul10  30574