Definition df-dp2 32033

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12677. (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 32032	. 2 class _𝐴𝐵
4		c1 11110	. . . . 5 class 1
5		cc0 11109	. . . . 5 class 0
6	4, 5	cdc 12676	. . . 4 class ;10
7		cdiv 11870	. . . 4 class /
8	2, 6, 7	co 7408	. . 3 class (𝐵 / ;10)
9		caddc 11112	. . 3 class +
10	1, 8, 9	co 7408	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1541	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32034  dp2eq2  32035  dp20u  32039  dp20h  32040  dp2cl  32041  dp2clq  32042  rpdp2cl  32043  dp2lt10  32045  dp2lt  32046  dp2ltsuc  32047  dp2ltc  32048  dpval  32051  dpfrac1  32053  dpval2  32054  dpval3  32055  dp3mul10  32059