Definition df-dp2 33325

Description: Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12741. (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 33324	. 2 class _𝐴𝐵
4		c1 11129	. . . . 5 class 1
5		cc0 11128	. . . . 5 class 0
6	4, 5	cdc 12740	. . . 4 class ;10
7		cdiv 11899	. . . 4 class /
8	2, 6, 7	co 7417	. . 3 class (𝐵 / ;10)
9		caddc 11131	. . 3 class +
10	1, 8, 9	co 7417	. 2 class (𝐴 + (𝐵 / ;10))
11	3, 10	wceq 1570	1 wff _𝐴𝐵 = (𝐴 + (𝐵 / ;10))

This definition is used by:  dp2eq1  33326  dp2eq2  33327  dp20u  33331  dp20h  33332  dp2cl  33333  dp2clq  33334  rpdp2cl  33335  dp2lt10  33337  dp2lt  33338  dp2ltsuc  33339  dp2ltc  33340  dpval  33343  dpfrac1  33345  dpval2  33346  dpval3  33347  dp3mul10  33351