Definition df-dp2 32946

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12636. (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 32945	. 2 class _𝐴𝐵
4		c1 11030	. . . . 5 class 1
5		cc0 11029	. . . . 5 class 0
6	4, 5	cdc 12635	. . . 4 class ;10
7		cdiv 11798	. . . 4 class /
8	2, 6, 7	co 7360	. . 3 class (𝐵 / ;10)
9		caddc 11032	. . 3 class +
10	1, 8, 9	co 7360	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1542	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32947  dp2eq2  32948  dp20u  32952  dp20h  32953  dp2cl  32954  dp2clq  32955  rpdp2cl  32956  dp2lt10  32958  dp2lt  32959  dp2ltsuc  32960  dp2ltc  32961  dpval  32964  dpfrac1  32966  dpval2  32967  dpval3  32968  dp3mul10  32972