Definition df-dp2 32792

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12650. (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 32791	. 2 class _𝐴𝐵
4		c1 11069	. . . . 5 class 1
5		cc0 11068	. . . . 5 class 0
6	4, 5	cdc 12649	. . . 4 class ;10
7		cdiv 11835	. . . 4 class /
8	2, 6, 7	co 7387	. . 3 class (𝐵 / ;10)
9		caddc 11071	. . 3 class +
10	1, 8, 9	co 7387	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1540	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is referenced by:  dp2eq1  32793  dp2eq2  32794  dp20u  32798  dp20h  32799  dp2cl  32800  dp2clq  32801  rpdp2cl  32802  dp2lt10  32804  dp2lt  32805  dp2ltsuc  32806  dp2ltc  32807  dpval  32810  dpfrac1  32812  dpval2  32813  dpval3  32814  dp3mul10  32818