Definition df-dp2 30574

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12087. (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 30573	. 2 class _𝐴𝐵
4		c1 10527	. . . . 5 class 1
5		cc0 10526	. . . . 5 class 0
6	4, 5	cdc 12086	. . . 4 class ;10
7		cdiv 11286	. . . 4 class /
8	2, 6, 7	co 7135	. . 3 class (𝐵 / ;10)
9		caddc 10529	. . 3 class +
10	1, 8, 9	co 7135	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1538	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  30575  dp2eq2  30576  dp20u  30580  dp20h  30581  dp2cl  30582  dp2clq  30583  rpdp2cl  30584  dp2lt10  30586  dp2lt  30587  dp2ltsuc  30588  dp2ltc  30589  dpval  30592  dpfrac1  30594  dpval2  30595  dpval3  30596  dp3mul10  30600